Upstream HasAdd

Class/HasAdd.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+module Class.HasAdd where
+
+open import Class.HasAdd.Core public
+open import Class.HasAdd.Instance public

Class/HasAdd/Core.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+module Class.HasAdd.Core where
+
+record HasAdd (A : Set) : Set where
+  infixl 6 _+_
+  field _+_ : A → A → A
+
+open HasAdd ⦃ ... ⦄ public

Class/HasAdd/Instance.agda

@@ -0,0 +1,21 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+module Class.HasAdd.Instance where
+
+open import Class.HasAdd.Core
+open import Data.Integer   as ℤ using (ℤ)
+open import Data.Nat       as ℕ using (ℕ)
+open import Data.Rational  as ℚ using (ℚ)
+open import Data.String    as Str
+
+instance
+  addInt : HasAdd ℤ
+  addInt ._+_ = ℤ._+_
+
+  addNat : HasAdd ℕ
+  addNat ._+_ = ℕ._+_
+
+  addRat : HasAdd ℚ
+  addRat ._+_ = ℚ._+_
+
+  addString : HasAdd String
+  addString ._+_ = Str._++_

standard-library-classes.agda

@@ -18,8 +18,10 @@ open import Class.DecEq.WithK public
 open import Class.Decidable public
 
 -- ** Others
-open import Class.Show public
 open import Class.Default public
+open import Class.HasAdd public
+open import Class.HasOrder public
+open import Class.Show public
 open import Class.ToBool public
 
 -- ** Tests