Add 型クラスは HAdd のヘルパでしかない?

[Seasawher]

Add だけでは分解できない

inductive MyNat : Type where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add (m n : MyNat) : MyNat :=
  match n with
  | zero => m
  | succ n => succ (add m n)

instance : OfNat MyNat 0 where
  ofNat := .zero

instance : OfNat MyNat 1 where
  ofNat := .succ .zero

instance : Add MyNat where
  add := MyNat.add

@[simp] theorem add_zero (n : MyNat) : n + 0 = n := by rfl
@[simp] theorem zero_add (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    dsimp [HAdd.hAdd, Add.add, MyNat.add] at ih ⊢
    rw [ih]

end MyNat