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

Question

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

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

没有得到错误：

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

有没有办法从内部访问那里的值？还是和要求ninside一样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