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?


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




All Articles