Idris - 在函數內部使用隱式變量

Question

我們如何在函數內部使用隱式變量？減少了最簡單的可能的情況下，是有可能有：

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

沒有得到錯誤：

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

是否有從內部訪問有值的方法？或者是在sin n裏面詢問n？

在這種情況下，是否有可能證明Vect是「雙射」並從那裏恢復變量？

Answer 1

確實沒有這樣的變量n，因爲它不受模式匹配限制。

你需要明確地將隱含變量範圍：

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

有可能在伊德里斯REPL來查看他們：

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