Idris - 在函数内部使用隐式变量

Question

我们如何在函数内部使用隐式变量？减少到最简单的情况,是否有可能:

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

没有得到错误:

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

有没有办法从里面获取价值？或者它与n内部要求相同sin n？

在这种情况下,是否有可能证明这Vect是一个"双射"并从那里恢复变量？

Answer 1

实际上没有这样的变量,n因为它不受模式匹配的限制.

您需要在范围中显式引入隐式变量:

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

可以在idris REPL中查看它们:

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