HAdd

HAdd は、+ という二項演算子のための型クラスです。 + 記法が何を意味するかについては制約はありません。

structure Colour where
  red : Nat
  blue : Nat
  green : Nat
  deriving Repr

def sample : Colour := { red := 2, blue := 4, green := 8 }

-- 最初は `+` 記号が定義されていないのでエラーになります。
/--
error: failed to synthesize
  HAdd Colour Colour ?m.1653
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in #eval sample + sample

/-- HAdd 型クラスのインスタンスを実装する -/
instance : HAdd Colour Colour Colour where
  hAdd c1 c2 := ⟨c1.red + c2.red, c1.blue + c2.blue, c1.green + c2.green⟩

-- 足し算記号が使えるようになった
#eval sample + sample