Почему Lean заставляет рекурсивные аргументы типа появляться после нерекурсивных?

Question

Следующее определение отклонено Lean:

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

с сообщением об ошибке "arg #2 of natlist.cons не является рекурсивным, но это происходит после рекурсивных аргументов"

И следующее определение принято, как и ожидалось:

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

В чем причина того, что Лин навязывает этот порядок?

Answer 1

Реализация индуктивных типов в Lean основана на статье "Dybjer" (1994) "Индуктивные семейства":

Бэкхаус [Bac88] и Coquand and Paulin [COP90] допустили несущественное обобщение, когда рекурсивные предпосылки могут предшествовать нерекурсивным. Я предпочитаю ставить все нерекурсивные предпосылки перед рекурсивными, поскольку первые здесь не могут зависеть от последних (но ситуация меняется в [Dyb92]). Это ограничение упрощает представление схемы и подчеркивает связь с порядком расположения.

Обратите внимание, что недавний коммит снимает это ограничение, и ваше первое определение работает сейчас.