Idris - 함수 내부에 암시 적 변수 사용

Question

함수 내부에서 암시 적 변수를 사용하려면 어떻게해야합니까?

dim : Vect n a -> Nat 
dim vec = n 

를 오류받지 않고 :

When elaborating right hand side of rep: 
No such variable n 

내부에서이 값에 액세스 할 수있는 방법이 있나요을 가장 단순한 경우에 감소, 그것을 가질 수 있습니다? 아니면 sin n 안에 n을 묻는 것과 같습니까?

이 경우 Vect이 "bijection"임을 증명하고 거기에서 변수를 복구 할 수 있습니까?

Answer 1

실제로 패턴 일치로 제한되지 않으므로 n과 같은 변수는 없습니다.

명시 적 범위에 암시 적 변수를 가져올 필요가

:

*> :set showimplicits 
*> :t dim 
Main.dim : {n : Prelude.Nat.Nat} -> {a : Type} -> 
    (__pi_arg : Prelude.Vect.Vect n a) -> Prelude.Nat.Nat