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

Question

следующее определение отвергается Lean:

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

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

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

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

В чем причина, по которой Lean применяет этот заказ? Реализация

Answer 1

Lean-х индуктивных типов на основе «Индуктивные семьи» бумаги П. Dybjer (1994):

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

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