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 

можно просмотреть их в Идрис РЕПЛ:

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