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)