From 7d5bd11ab34f189fa51e89110de771a4399341e3 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Tue, 11 Jun 2024 06:29:49 +0200
Subject: [PATCH] [ feat for #108 ] IsLawfulNum instance for Int

---
 lib/Haskell/Law/Num/Int.agda  | 27 +++++++++++++++++++++++++++
 lib/Haskell/Law/Num/Word.agda |  1 +
 2 files changed, 28 insertions(+)
 create mode 100644 lib/Haskell/Law/Num/Int.agda

diff --git a/lib/Haskell/Law/Num/Int.agda b/lib/Haskell/Law/Num/Int.agda
new file mode 100644
index 00000000..91f617f0
--- /dev/null
+++ 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
index 30aaf246..7e95de01 100644
--- 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