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