为什么Lean强制递归类型参数在非递归类型参数后出现？

Question

下面的定义是由精益拒绝：

inductive natlist 
| nil : natlist 
| cons: natlist → ℕ → natlist 

与错误消息“ARG＃ 'natlist.cons' 的2不是递归的，但它的递归参数之后发生”

如预期的那样，接受以下定义：

inductive natlist 
| nil : natlist 
| cons: ℕ → natlist → natlist 

Lean执行此命令的原因是什么？

Answer 1

精益的实现感应类型的基于由P. Dybjer的“感应家庭”纸（1994）：

巴克豪斯[Bac88]和Coquand和波林[COP90]允许的无关紧要的概括，其中递归处所可能会先于非递归的。我倾向于在递归之前放置所有非递归的前提，因为前者在这里不能依赖后者（但[Dyb92]中的情况发生变化）。这种限制简化了方案的表述，并强调了与有序的关系。

请注意，最近的commit删除了此限制，现在您的第一个定义可以使用。