variables (P Q:Prop) theorem sample (hp : P) (hq : Q) : P ∧ Q ∧ P := begin apply and.intro, -- 5 assumption, -- 4 apply and.intro, -- 3 assumption, -- 2 assumption -- 1 endtry it! ☆ ☆ ---------- 1 ---------- 2 P, Q → P P, Q → Q ☆ ---------…

ゴールズ状態にはカーソルがあって、現ゴールが決まっている。それは表示上の一番上または一番左のゴールで、アタック（タクティクの適用）は常に現ゴールに対して行われる。したがって、逆リーズニングツリーを上から下、左から右に描けば、上から下の方向…

コンテキスト内のセットアップではない型宣言を仮説〈hypothesis〉と呼ぶ。ラムダリスト内の型宣言を仮定〈assumption〉と呼ぶ。だが、仮説によりターゲットが直接得られるときにう使うタクティク名は premise, hypothesis ではなくて、asspumption （by ass…

Leanのシーケントは、ゴール＝リクエストとして出てくるが、その形式は コンテキスト ⊢ ターゲット コンテキストは型宣言のカンマ区切り列、ターゲットは型式〈かたしき〉。その意味はリクエストだから、 コンテキスト ⊢? _:ターゲット 例： p q : Prop, hp …

https://leanprover.github.io/reference/tactics.htmlを見ても、自然言語で書いてあるだけ。これでは分からない！！順行リーズニングと逆行リーズニングをペアにして、絵で説明しないと。

id : an identifier expr : an expression : a sequence of identifiers and expressions (a : α) where a is an identifier and α is a Type or a Prop. バインダーズは、列となっている。列とリストの区別はあるのかな？ 列＝構文上のリスト かな？ Leanで…

format or template plan and materials performance or execution performer schedule media or channel

Ireneではない。ideal Lean 理想化Lean。 Lean ILean 圏論 論理 A→B→C A B → C [A, B → C] A⊃B⊃C or A∧B⊃C (a:A)(b:B):C A B ⇒ C A, B → C A, B → C f (a:A)(b:B):C f (A B) ⇒ C f: A, B → C f: A, B → C (a:A)(b:B)⊢ C A B ⊢? C - - f:A → B f ()⇒A→B f:ε →…