From d944cb444e3d02d94fc34090915097b5ff5707e7 Mon Sep 17 00:00:00 2001
From: whatisRT <andre.knispel@gmx.de>
Date: Fri, 11 Oct 2024 14:59:56 +0200
Subject: [PATCH] Upstream HasAdd

---
 Class/HasAdd.agda             |  5 +++++
 Class/HasAdd/Core.agda        |  8 ++++++++
 Class/HasAdd/Instance.agda    | 21 +++++++++++++++++++++
 standard-library-classes.agda |  4 +++-
 4 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 Class/HasAdd.agda
 create mode 100644 Class/HasAdd/Core.agda
 create mode 100644 Class/HasAdd/Instance.agda

diff --git a/Class/HasAdd.agda b/Class/HasAdd.agda
new file mode 100644
index 0000000..917f7bd
--- /dev/null
+++ b/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
diff --git a/Class/HasAdd/Core.agda b/Class/HasAdd/Core.agda
new file mode 100644
index 0000000..061ed12
--- /dev/null
+++ b/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
diff --git a/Class/HasAdd/Instance.agda b/Class/HasAdd/Instance.agda
new file mode 100644
index 0000000..d8b6412
--- /dev/null
+++ b/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._++_
diff --git a/standard-library-classes.agda b/standard-library-classes.agda
index c2c6653..6b92c14 100644
--- a/standard-library-classes.agda
+++ b/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