variable (α : Type) variable (F G : α → Type) def f : (∀ x : α, F x × G x) → (∀ y : α, F y) := fun h : ∀ x : α, F x × G x => fun y : α => (h y).fst関数ヘッドを変形すると： variable (α : Type) variable (F G : α → Type) def f' (h : ∀ x : α, …

Lean 4ではキーワードを整理したらしく。 constantが廃止されて、axiomのみを使うようになった。 Πが廃止されて、∀のみを使うようになった。 assumeが廃止されて、funまたはλのみを使うようになった。 variables は廃止。variable が使える。 parameter, par…

Leanマニュアルでは "object" も使っているが、混乱のもとなので「要素〈element〉」を使う。「インスタンス」も混乱のもとなので使わない。「型の要素」を使う。型の要素が命題の証拠〈witness〉に対応する。次はセクションの定義： variable (F : Type → T…