constructor
#Fleeting_Notes
constructor
Leanのconstructorについて
constructorの訳は構成子かも
from: 『Homotopy Type Theory 入門』
関連: 型構築子
code:lean.hs
example (hP : P) (hQ : Q) : P ∧ Q := by
-- たとえばゴールが論理積の場合、constructorによってゴールが分岐する。
-- 分岐したゴールたちには名前がついていて、caseを使ってそれぞれのゴールに的を絞ることができる。
constructor
case left =>
apply hP
case right =>
apply hQ
確認用
Q. constructor
メモ
Structures - Functional Programming in Lean
constructor - Tactic Reference
constructor: 論理積や同値性を示す - Lean by Example
調査用
Google.icon constructor(日)
Google.icon constructor Lean(日)
Google.icon Constructor(英)
Google.icon Constructor Lean(英)
Wikipedia.icon
constructor - Wikipedia(日)
constructor(検索) - Wikipedia(日)
Wikipedia.icon
Constructor - Wikipedia(英)
Constructor(検索) - Wikipedia(英)