[ feat for #108 ] IsLawfulNum instance for Int

agda · Jul 9, 2024 · 7d5bd11 · 7d5bd11
1 parent 71e8ab3
commit 7d5bd11
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 0 deletions.
diff --git a/lib/Haskell/Law/Num/Int.agda b/lib/Haskell/Law/Num/Int.agda
@@ -0,0 +1,27 @@
+module Haskell.Law.Num.Int where
+
+open import Haskell.Prim using (refl; tt)
+open import Haskell.Prim.Num
+open import Haskell.Prim.Int
+open import Haskell.Prim.Word
+
+open import Haskell.Law.Num
+open import Haskell.Law.Num.Word
+
+instance
+  open NumHomomorphism
+  open NumEmbedding
+
+  iNumEmbeddingIntWord : NumEmbedding Int Word intToWord int64
+  +-hom          (hom iNumEmbeddingIntWord) (int64 _) (int64 _) = refl
+  *-hom          (hom iNumEmbeddingIntWord) (int64 _) (int64 _) = refl
+  minus-ok       (hom iNumEmbeddingIntWord) = tt
+  negate-ok      (hom iNumEmbeddingIntWord) = tt
+  fromInteger-ok (hom iNumEmbeddingIntWord) = tt
+  0-hom          (hom iNumEmbeddingIntWord) = refl
+  1-hom          (hom iNumEmbeddingIntWord) = refl
+  negate-hom     (hom iNumEmbeddingIntWord) (int64 _) = refl
+  embed               iNumEmbeddingIntWord  (int64 _) = refl
+
+  iLawfulNumInt : IsLawfulNum Int
+  iLawfulNumInt = map-IsLawfulNum intToWord int64 iNumEmbeddingIntWord iLawfulNumWord
diff --git a/lib/Haskell/Law/Num/Word.agda b/lib/Haskell/Law/Num/Word.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Haskell.Law.Num.Word where
 
 open import Haskell.Prim