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

Question

以下定义被 Lean 拒绝:

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] and Coquand and Paulin [COP90] allowed the inessential generalisation where recursive premises may precede non-recursive ones. I prefer to put all non-recursive premises before the recursive ones, since the former cannot depend on the latter here (but the situation changes in [Dyb92]). This restriction simplifies the presentation of the scheme and emphasises the relationship with the well-orderings.

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