formaltt:类型理论的形式化

简单类型理论的形式化 编码标准 我们在这里收集一些编码标准。 仅import必要的内容。 避免全局open而希望使用本地open语句。 线条不要太长。 没有很好的理由，不要重命名标准库中的内容。 如果发现库中已经存在某些东西，请直接使用它，而不要通过重命名来使用它。 是的，这意味着需要更多的工作来重命名代码中的内容，但同时也避免了创建意大利面条。 我们追求的想法概述 在这个项目中，我们旨在将阿格达中的简单类型理论形式化。 我们可以沿着一般性和荟萃分析这两个轴进行研究。 概论 普遍性是关于我们所涵盖的一类类型理论有多大。 衡量“一般性”的方法有很多，但这是一种应该能很好地工作并使我们逐步进行的方法。 单分类代数理论 参数化方式： 一族术语符号，每个符号都有一个Arity（集合或数字） 一个家庭等式公理Γ ⊢ ℓ ≡ r见下文 表达式： 项s ， t ： 评判形式： 形式 意