Idris是否與Agda的`_`表達式等價？

Question

除了具有隱含參數之外，Agda還允許您省略顯式參數的值並將其替換爲由_字符表示的元變量，其值將通過與隱式解析相同的過程來確定。

Idris是否有類似的功能，或者是隱式參數是將元變量引入程序的唯一方式？

Answer 1

您也可以在Idris中使用_。

import Data.Vect 

foo : (n : Nat) -> Vect n a -> Vect n a 
foo n xs = xs 

bar : Vect 3 Nat 
bar = foo _ [1, 2, 3] -- works