From 50de317f40f38877acbb77d58f007302049ab602 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 5 Nov 2024 01:56:51 +0900
Subject: [PATCH] =?UTF-8?q?HAdd=20=E5=9E=8B=E3=82=AF=E3=83=A9=E3=82=B9?=
 =?UTF-8?q?=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B=20Fixes=20#1054?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/TypeClass/HAdd.lean | 27 +++++++++++++++++++++
 booksrc/SUMMARY.md                          |  1 +
 2 files changed, 28 insertions(+)
 create mode 100644 LeanByExample/Reference/TypeClass/HAdd.lean

diff --git a/LeanByExample/Reference/TypeClass/HAdd.lean b/LeanByExample/Reference/TypeClass/HAdd.lean
new file mode 100644
index 0000000..ef4d25d
--- /dev/null
+++ b/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
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 4bbb3e8..63a4aa1 100644
--- a/booksrc/SUMMARY.md
+++ b/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)