まだ未整理だが、とりあえず備忘メモ。まず、対称性がある操作達。 無制限タプル構成 無制限コタプル構成（無制限タプル構成の双対） 有限タプル構成（無制限から制限） 有限コプル構成（有限タプル構成の双対） 依存カリー化 カリー化（依存カリー化の非依…

フォワード・リーズニング用に、ステージと同じコンビネータ・コマンドがある： 連言導入用コンビネータ： 既存のn個の証明から連言への証明を作る。 全称導入用コンビネータ： 既存のパラメータ付き証明から全称への証明を作る。 選言除去用コンビネータ： …

Leanでは 対応する閉じ括弧をハイライトするとか、"go to bracket"コマンド（[ctrl+shift+\]）がうまく動かない。なにしろ、begin/endの括弧を使わない方針だから。