HAdd
HAdd
(heterogeneous addition)は、+
という二項演算子のための型クラスです。
+
記法が何を意味するかについては制約はありません。
任意の型 α, β, γ : Type
に対して足し算 (· + ·) : α → β → γ
を定義することができます。
structure Colour where
red : Nat
blue : Nat
green : Nat
deriving Repr
def sample : Colour := { red := 2, blue := 4, green := 8 }
-- メタ変数の番号を表示しない
set_option pp.mvars false
-- 最初は `+` 記号が定義されていないのでエラーになる
/--
error: failed to synthesize
HAdd Colour Colour ?_
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