定义数据类型时，我可以在冒号之前“传递”一些参数。
data Image_э_ { A B : Set} : (f : A → B) → B → Set where
im : {f : A → B} → (x : A) → Image f э f x
但出于未知原因，我似乎无法在函数声明中执行此操作。
exIm {A B : Set} : {f : A → B}{y : B} → Image f э y → B
exIm {y = y} _ = y
在冒号之前和之后传递参数的根本区别是什么？老实说，我不知道为什么有人想在冒号之前传递参数以及它可以带来什么好处。也许，这样的数据类型定义使得冒号之前的参数在构造函数中可见。
我不知道为什么有人想在冒号之前传递参数
以及它可以带来什么优势。
在数据类型声明中，冒号之前传递的参数在范围内
数据类型定义的主体。
我认为这将是一个很好的功能请求。我们可以有例如
typeOf {A : Set} : A -> Set
typeOf a = A -- A is in scope because `{A : Set}` was before the colon
因此，请随意打开一个新问题来建议更改：https://github.com/agda/agda/issues https://github.com/agda/agda/issues
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
