強制自動フルカリー化

Leanの定義構文のプロファイル部は完全なシンタックスシュガーで、無視されて、内部的にはフルカリー化版が記憶される。

そそもそも、内部の還元エンジン〈reductione engine〉がフルカリー化されたポイント射しか扱えない。これが、圏論的解釈とラムダ計算的解釈のギャップになっている。とんでもないギャップかも知れない。