aboutsummaryrefslogtreecommitdiff
path: root/Prelude
diff options
context:
space:
mode:
Diffstat (limited to 'Prelude')
-rw-r--r--Prelude/Number.agda60
1 files changed, 60 insertions, 0 deletions
diff --git a/Prelude/Number.agda b/Prelude/Number.agda
new file mode 100644
index 0000000..02024d0
--- /dev/null
+++ b/Prelude/Number.agda
@@ -0,0 +1,60 @@
+{- Copyright © 2015 Benjamin Barenblat
+
+Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
+this file except in compliance with the License. You may obtain a copy of the
+License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software distributed
+under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
+CONDITIONS OF ANY KIND, either express or implied. See the License for the
+specific language governing permissions and limitations under the License. -}
+
+module B.Prelude.Number where
+
+import Algebra
+import Data.Integer
+import Data.Integer.Properties
+import Data.Nat
+import Data.Nat.Properties
+open import Level using (_⊔_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open Data.Integer using (ℤ) public
+open Data.Nat using (ℕ) public
+
+record NearSemiring {c} {ℓ} (A : Set c) : Set (Level.suc (c ⊔ ℓ)) where
+ field
+ structure : Algebra.NearSemiring c ℓ
+ typeEquality : A ≡ Algebra.NearSemiring.Carrier structure
+
+NearSemiringInstance : ∀ {c ℓ}
+ → (structure : Algebra.NearSemiring c ℓ)
+ → NearSemiring (Algebra.NearSemiring.Carrier structure)
+NearSemiringInstance structure =
+ record { structure = structure; typeEquality = refl }
+
+private
+ change₂ : ∀ {c ℓ A′}
+ → ⦃ witness : NearSemiring {c} {ℓ} A′ ⦄
+ → ((r : Algebra.NearSemiring c ℓ)
+ → let A = Algebra.NearSemiring.Carrier r in
+ A → A → A)
+ → A′ → A′ → A′
+ change₂ ⦃ witness ⦄ f rewrite NearSemiring.typeEquality witness =
+ f (NearSemiring.structure witness)
+
+_*_ : ∀ {c ℓ A} → ⦃ _ : NearSemiring {c} {ℓ} A ⦄ → A → A → A
+_*_ = change₂ Algebra.NearSemiring._*_
+
+instance
+ NearSemiring-ℕ : NearSemiring ℕ
+ NearSemiring-ℕ =
+ NearSemiringInstance (Algebra.CommutativeSemiring.nearSemiring
+ Data.Nat.Properties.commutativeSemiring)
+
+ NearSemiring-ℤ : NearSemiring ℤ
+ NearSemiring-ℤ =
+ NearSemiringInstance (Algebra.CommutativeRing.nearSemiring
+ Data.Integer.Properties.commutativeRing)