Имеет ли Идрис эквивалент выражения `_` Агды?

Question

Помимо наличия неявных аргументов, Agda позволяет вам опустить значение явного аргумента и заменить его метапеременной, обозначаемой символом _, значение которого затем определяется с помощью той же процедуры, что и неявное разрешение.

Есть ли у Идриса аналогичная функция или неявные аргументы - единственный способ введения метапеременных в программы?

Answer 1

Вы также можете использовать _ в Идрисе.

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