recursion - 为什么精益强制递归类型参数出现在非递归参数之后？

Question

精益拒绝以下定义：

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

带有错误消息“'natlist.cons' 的 arg #2 不是递归的，但它发生在递归参数之后”

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

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

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

Answer 1

Lean 对归纳类型的实现基于 P. Dybjer (1994) 的“归纳系列”论文：

Backhouse [Bac88] 和 Coquand 和 Paulin [COP90] 允许递归前提可能先于非递归前提的非本质概括。我更喜欢将所有非递归前提放在递归前提之前，因为前者在这里不能依赖于后者（但 [Dyb92] 中的情况发生了变化）。这种限制简化了方案的表示，并强调了与良序的关系。

请注意，最近的提交删除了此限制，您的第一个定义现在有效。