Does Idris have an equivalent to Agda's `_` expressions?

Question

In addition to having implicit arguments, Agda lets you omit the value of an explicit argument and replace it with a metavariable, denoted by the _ character, whose value is then determined through the same procedure as implicit resolution.

Does Idris have a similar feature, or are implicit arguments the only way of introducing metavariables into programs?

Answer 1

You can use _ in Idris as well.

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