ptt:用于内部参数类型理论的实验类型检查器

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