我本着本文的精神实现了依赖类型的 lambda 演算:http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf微积分有效，我用它进行了实验并扩展了几件事:许多宇宙，硬编码归纳公理。但是，我想添加归纳类型来做更复杂的事情。
我正在考虑两种方法
- 介绍 Fin-N、Product 和 W 类型，并用它们表示归纳类型。
- 生成归纳和递归公理。
这两种方式我都不喜欢。第一个太低级，需要付出大量努力才能从高级语言转换为核心语言。第二种方法工作量很大，而且容易出错，因为复杂归纳类型的递归原理的生成有很多极端情况，即正/负出现。
如何做到这一点？这些类型在 Coq、Agda 和 Idris 等现有系统中是如何实现的？
最佳答案
抱歉，我不了解 Idris。
对于 Agda，我推荐 Ulf Norell Phd Thesis作为起点，但此后系统不断发展。
Coq 在您的列表中引入了第三个项目符号:自动生成的谓词。
每个归纳类型都带有 3 个(在某些特殊情况下为 1 个)自动为用户定义的归纳方案，并命名为 your_type_rect、your_type_rec 和 your_type_ind(特殊情况下只有后一种)。这些是语言的实际术语，为用户自动生成，并由 induction 策略使用(我对最后一个不是 100% 确定)，而不是公理。
其实你可以关闭这个自动生成，自己写你的归纳方案。
可以找到一些关于induction 的文档here .我建议您在 Coq 邮件列表上提问，开发人员可能会给您更多关于 Coq 内部结构的见解。
最好的， 五、
关于coq - 代表归纳类型，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22340809/