Idris有类似于Agda的“_”表达式的等效物吗？

Question

除了隐式参数之外，Agda 还允许你省略显式参数的值，并将其替换为一个元变量。元变量用 _ 表示，其值是通过与隐式解析相同的过程来确定的。

Idris 是否有类似的功能，或者隐式参数是否是引入程序中元变量的唯一方法？

- jmite

Answer 1

在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

- Andy Morris

---

看起来我错过了这个，因为我有其他语法错误，所以认为它是无效的！无论如何，这并没有被清楚地记录下来。谢谢！ - jmite