idr-logical-foundations:伊德里斯的逻辑基础

伊德里斯的逻辑基础 这是本杰明·皮尔斯（Benjamin C. Pierce）等人在Coq中的《逻辑基础》的翻译。 它还可能会使用Idris（2016）中的Software Foundations作为参考。 要求 伊德里斯 Pandoc（可选） 制作（可选） 字体：蒙特塞拉特，费拉Sans和费拉代码（可选） 建造 只需make ，它将根据book/的来源进行类型检查并创建PDF文件。 解决经验 重要提示：根据本杰明·皮尔斯（Benjamin C. Pierce）的要求，请勿在公共媒体上发布您的解决方案。 （包括GitHub / GitLab / etc） 只需为您的解决方案替换类型Kong（ ?type_hole ），然后运行make test即可运行类型检查器。 这项工作是根据