apply は backward apply〈deapply | reverse apply〉の意味。だいぶ困る。 複数のゴールは左〈上〉から順に攻撃する。ツリー辿りは深さ優先再帰かな。 ゴールの固有名はないが、left, right のcaseラベルは付く。並びの順番でも参照できる。 ツリーが構成さ…

git init 直後HEADの内容： ref: refs/heads/mainmainという名前はここで決定されて、その後も使われる。初期化しただけでは ./.git/refs/heads/ は空で、HEADの参照先である ./.git/refs/heads/main は存在しない。git add README.md しても見た目上の「リ…

The formal proof on the other side was a big and unreadable 'proof term' 出典： 不明、現在はインターネット上にないようだ。

証明図から証明項に引き写すのは手作業。支援系とかいいながら、ソフトウェアは何も支援してくれない。 /-! example_1.lean -/ namespace Imp def elim_right {A B: Prop} (f:A → B) (a:A) : B := f a def elim_left {A B: Prop} (a:A) (f:A → B) : B := f a…