Hat Idris ein Äquivalent zu Agdas `_` Ausdrücken?

Question

Zusätzlich zu impliziten Argumenten können Sie mit Agda den Wert eines expliziten Arguments weglassen und durch eine Metavariable ersetzen, die mit dem Zeichen _ gekennzeichnet ist und deren Wert dann durch dieselbe Prozedur wie die implizite Auflösung bestimmt wird.

Hat Idris eine ähnliche Funktion oder sind implizite Argumente die einzige Möglichkeit, Metavariablen in Programme einzuführen?

Answer 1

Sie können auch _ in Idris verwenden.

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