search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
49 stars 7 forks source link

Pair が関手（functor）であることを示す例 #1154

Open Seasawher opened 16 hours ago

Seasawher commented 16 hours ago 
/-- 与えられた型の対を作る -/
def Pair (α : Type) : Type := α × α

/-- `Pair` を関手にする -/
instance : Functor Pair where
  map f := fun a => (f a.fst, f a.snd)

macro "functor" : tactic => `(tactic| constructor <;> aesop)

instance : LawfulFunctor Pair := by 
  functor