文件名称：ECC:罗的 ECC 浅嵌入 Agda
文件大小：28KB
文件格式：ZIP
更新时间：2024-07-11 20:09:44
Agda
ECC-in-Agda 这是在 Agda 中形式化 [An Extended Calculus of Constructions] (citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.5883) 的尝试。 开发包含一个不可预测的宇宙，即位于其中的unit类型，自然数，无限宇宙层次结构，由自然数索引，Sigma 和 Pi 类型，有界从属量词和 Agda 风格的显式Lift ， lift和lower ，用于使包含规则可被接受。 快速品尝 这是I组合子： I : Term (type 0 Π λ A -> A ⟶ A) I = ⇧ λ _ -> ⇧ λ x -> ↑ x Agda 的λ用作绑定器，因此开发中不包含 De Bruijn 索引。 Π是一个中缀运算符。 ⟶是Π的非依赖版本。 ⇧是Term数据类型的构造函数，应用于类型为(x
【文件预览】：
ECC-master
----ECC()
--------Main.agda(234B)
--------Terms()
--------Tag.agda(888B)
--------Utilities.agda(112B)
--------Tests()
--------Types()
----readme.md(16KB)
----readme.agda(17KB)