왜 Lean은 재귀 적 형식 인수를 비 반복적 형식 뒤에 표시 할 것을 강요합니까?

Question

다음 정의는 린에 의해 거부되어 오류 메시지와

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

에게 " 'natlist.cons'의 2가 순환되지 인수 번호를하지만 재귀 인수 후 발생"

다음과 같은 정의가 예상대로 수용됩니다.

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

Lean이이 주문을 시행하는 이유는 무엇입니까? 유도 성 타입의

Answer 1

린 구현 P. Dybjer 의한 "유도 패밀리"용지 (1994)에 기초한다 :

변소 [Bac88] 및 Coquand 및 Paulin의 [COP90]는 중요하지 않은 일반화 허용 여기서 재귀 소재지 비 재귀 적 행보에 선행 할 수있다. 이전의 재귀 적 재사용을 재귀 적 재귀 재귀에 의존 할 수 없기 때문에 재귀 적 재귀 재귀에 앞서 모든 재귀 적 재귀를 배치하는 것을 선호합니다 (그러나 [Dyb92]의 상황이 바뀜). 이 제한은 계획의 표현을 단순화하고 잘 - 정렬과의 관계를 강조한다.

최근 commit은이 제한을 없애고 첫 번째 정의가 작동한다는 점에 유의하십시오.