Lean 4 では証明の中で現在証明している定理を利用できる。
つまり再帰できるわけだが、Lean は一般の再帰はできない (recursor しか使えない) はずなので、 equation compiler がどうやってコンパイルしているのか気になる。
これはどうやっているか調べると、 構造再帰で済む場合には帰納型の recursor を使い、 それでは済まない場合は整礎帰納法になるようだ。 整礎帰納法の場合、引数が小さくなることの証明が必要だが、簡単な場合は自動証明で済み、そうでなければ人間が与える、ということらしい。
[latest]