文件名称：ptt:用于内部参数类型理论的实验类型检查器
文件大小：71KB
文件格式：ZIP
更新时间：2024-05-30 00:19:12
OCaml
ptt 通过评估（nbe）和语义类型检查对具有n元内部参数的Martin-Löf类型理论进行归一化的实验实现。 该存储库以 （一种依赖于模式的类型理论的实现）为基础； 模态结构已被删除，并替换为内部参数原语。 此处实施的类型理论大致上是的类型理论，但是它基于内涵式Martin-Löf类型理论而不是立方类型理论。 因此，它又与相似。 出于实现方面的考虑，相对于这些理论的一个变化是，将Gel /β型公式化为肯定的（具有消除原理）而不是否定的（具有推论和eta原理）。 为了进行实验，我们为每个（具体） n包含n元参数原语。 但是，我们观察到，迭代二进制参数足以对所有n进行n元参数编码。 不同Arity的参数原语之间没有直接交互。 有关示例，请参见test/目录。 句法 句法 描述 [x] A {a0; ...; an} 跨度为x且端点为a1 ，...， an A的桥的类型 bri x
【文件预览】：
ptt-master
----ptt.opam(212B)
----src()
--------lib()
--------bin()
----dune-project(35B)
----LICENSE(1KB)
----test()
--------church_naturals.ptt(2KB)
--------line.ptt(791B)
--------no-wlem.ptt(4KB)
--------gel.ptt(2KB)
--------codisc.ptt(4KB)
--------identity.ptt(513B)
--------binary_to_quarternary.ptt(3KB)
--------no-lem.ptt(9KB)
--------n-ary.ptt(2KB)
--------relativity.ptt(4KB)
--------extent.ptt(4KB)
--------const_nat.ptt(5KB)
--------leibniz.ptt(4KB)
--------nat_nullary_const.ptt(2KB)
--------queue.ptt(35KB)
--------bch.ptt(39KB)
--------basic.ptt(697B)
--------discrete.ptt(6KB)
----test.sh(138B)
----README.md(3KB)
----Makefile(243B)
----.gitignore(5KB)