constructor
#Fleeting_Notes
constructor
Leanのconstructorについて
code:lean.hs
example (hP : P) (hQ : Q) : P ∧ Q := by
-- constructorによってゴールが分岐する。分岐したゴールたちには名前がついていて、caseを使って
-- それぞれのゴールに的を絞ることができる。
constructor
case left =>
apply hP
case right =>
apply hQ
確認用
Q. constructor
調査用
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(英)