Idris ha un equivalente alle espressioni `_` di Agda?

Question

Oltre ad avere argomenti impliciti, Agda consente di omettere il valore di un argomento esplicito e sostituirlo con una metavariabile, indicata dal carattere _, il cui valore viene quindi determinato mediante la stessa procedura della risoluzione implicita.

Idris ha una caratteristica simile o sono argomenti impliciti l'unico modo di introdurre metavariabili nei programmi?

Answer 1

È possibile utilizzare anche _ in 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