HAdd 型クラスを紹介する

LeanByExample/Reference/TypeClass/HAdd.lean

@@ -0,0 +1,27 @@
+/- # 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

booksrc/SUMMARY.md

@@ -86,6 +86,7 @@
   - [Decidable: 決定可能](./Reference/TypeClass/Decidable.md)
   - [Functor: ファンクタ](./Reference/TypeClass/Functor.md)
   - [GetElem: n番目の要素を取得](./Reference/TypeClass/GetElem.md)
+  - [HAdd: + のための記法クラス](./Reference/TypeClass/HAdd.md)
   - [Inhabited: 有項にする](./Reference/TypeClass/Inhabited.md)
   - [OfNat: 数値リテラルを使用](./Reference/TypeClass/OfNat.md)
   - [Repr: 表示方法を指定](./Reference/TypeClass/Repr.md)