如何解决阿格达冒号之前/之后的参数
在定义数据类型时,我可以在冒号前“传递”一些参数。
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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。