gpt4 book ai didi

agda - Idris 是否与 Agda 的 `_` 表达式等效?

转载 作者:行者123 更新时间:2023-12-04 18:04:05 25 4
gpt4 key购买 nike

除了具有隐式参数之外,Agda 还允许您省略显式参数的值并将其替换为元变量,用 _ 表示。字符,然后通过与隐式解析相同的过程确定其值。

Idris 是否有类似的特性,或者隐式参数是将元变量引入程序的唯一方法?

最佳答案

您可以使用 _在 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

关于agda - Idris 是否与 Agda 的 `_` 表达式等效?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/35927888/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com