Leanは、再帰型引数を非再帰型引数の後に表示するように強制するのはなぜですか？

Question

次の定義は、リーンによって拒否されます。エラーメッセージと

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

「『natlist.cons』の＃2引数は再帰的ではありませんが、それは再帰的な引数の後起こる」

をそして、次の定義が期待どおりに受け入れられます。

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

リーンがこの注文を強制する理由は何ですか？誘導タイプのの

Answer 1

リーン実装はP. Dybjerによる「誘導家族」紙（1994）に基づいています。

Backhouse [Bac88]とCoquandとポーリン[COP90]は非本質的一般化を許可した場合に、再帰的な施設非再帰的なものに先行してもよい。私は再帰的なものの前にすべての非再帰的な前提を置くことを好みます、なぜなら前者は後者に依存できないからです（しかし、[Dyb92]の状況が変わります）。この制限は、制度の提示を簡素化し、秩序との関係を強調する。

最近のcommitではこの制限がなくなり、最初の定義が正常に機能することに注意してください。