Does Idris have the equivalent of Agda `_` expressions?

Question

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

Does Idris have a similar function or implicit arguments the only way to introduce meta variables into programs?

Answer 1

You can use _ in Idris.

 import Data.Vect foo : (n : Nat) -> Vect na -> Vect na foo n xs = xs bar : Vect 3 Nat bar = foo _ [1, 2, 3] -- works