[如果有人希望重新实现归纳构造的演算，那么实现这一目标的“最短”途径是什么？特别是，内核中的实际上会继续运行是什么？
我的心智模型说我们需要两件事：
但是，由于语言是依赖类型的，因此类型检查器很可能会取决于确定两种类型相等时的计算能力。
所以，实际上，Coq评估程序的操作语义]是什么？什么是类型检查推断规则
？它们实施起来有多困难？我想要这两个事实的稳定，标准的参考，因此我可以重新实现一个小的CIC内核。
如果有人希望重新实现归纳构造的演算，那么实现这一目标的“最短”途径是什么？特别是内核内部到底发生了什么？我的心理模型说我们...
听起来有点像自我广告，但值得一看一下metacoq项目https://metacoq.github.io/metacoq/（或直接在github repo https://github.com/MetaCoq/metacoq）。以及与之相关的论文。我们指定Coq的类型理论（现在为负η，模板多态性和模块），并为其编写声音类型检查器。
因此，我同意一个关键因素是能够[[compare