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