Idris - using an implicit variable inside a function
How can we use an implicit variable inside a function? Reduced to the simplest possible case, is it possible:
dim : Vect n a -> Nat
dim vec = n
without getting error:
When elaborating right hand side of rep:
No such variable n
Is there a way to access these values from the inside? Or is it the same as asking n
inside sin n
?
In this case, is it possible to prove what Vect
is a "bijection" and restores the variables there?
+3
source to share
1 answer
There is no such variable n
as it is not limited to pattern matching.
You need to explicitly inject implicit variables into the scope:
dim : Vect n a -> Nat
dim {n} vec = n
These can be viewed in the idris REPL:
*> :set showimplicits
*> :t dim
Main.dim : {n : Prelude.Nat.Nat} -> {a : Type} ->
(__pi_arg : Prelude.Vect.Vect n a) -> Prelude.Nat.Nat
+6
source to share