Switch Positive/Negative/etc. to use irrelevant instance arguments (#1581)

Author: MatthewDaggitt

CHANGELOG.md

@@ -14,7 +14,7 @@
 
 module Data.Integer.Base where
 
-open import Data.Bool.Base using (Bool; true; false)
+open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤)
 open import Data.Nat.Base as ℕ
@@ -127,23 +127,39 @@ _≤ᵇ_ : ℤ → ℤ → Bool
 NonZero : Pred ℤ 0ℓ
 NonZero i = ℕ.NonZero ∣ i ∣
 
-Positive : Pred ℤ 0ℓ
-Positive +[1+ n ] = ⊤
-Positive +0       = ⊥
-Positive -[1+ n ] = ⊥
+record Positive (i : ℤ) : Set where
+  field
+    pos : T (1ℤ ≤ᵇ i)
 
-Negative : Pred ℤ 0ℓ
-Negative (+ n)    = ⊥
-Negative -[1+ n ] = ⊤
+record NonNegative (i : ℤ) : Set where
+  field
+    nonNeg : T (0ℤ ≤ᵇ i)
 
-NonPositive : Pred ℤ 0ℓ
-NonPositive +[1+ n ] = ⊥
-NonPositive +0       = ⊤
-NonPositive -[1+ n ] = ⊤
+record NonPositive (i : ℤ) : Set where
+  field
+    nonPos : T (i ≤ᵇ 0ℤ)
 
-NonNegative : Pred ℤ 0ℓ
-NonNegative (+ n)    = ⊤
-NonNegative -[1+ n ] = ⊥
+record Negative (i : ℤ) : Set where
+  field
+    neg : T (i ≤ᵇ -1ℤ)
+
+-- Instances
+
+instance
+  pos : ∀ {n} → Positive +[1+ n ]
+  pos = _
+
+  nonNeg : ∀ {n} → NonNegative (+ n)
+  nonNeg = _
+
+  nonPos0 : NonPositive 0ℤ
+  nonPos0 = _
+
+  nonPos : ∀ {n} → NonPositive -[1+ n ]
+  nonPos = _
+
+  neg : ∀ {n} → Negative -[1+ n ]
+  neg = _
 
 -- Constructors
 

src/Data/Integer/Base.agda

@@ -90,7 +90,7 @@ a≡a%ℕn+[a/ℕn]*n n@(-[1+ _ ]) d with ∣ n ∣ ℕ.% d in eq
 
 [n/ℕd]*d≤n : ∀ n d .{{_ : ℕ.NonZero d}} → (n divℕ d) * + d ≤ n
 [n/ℕd]*d≤n n d = let q = n divℕ d; r = n modℕ d in begin
-  q * + d        ≤⟨  n≤m+n r ⟩
+  q * + d        ≤⟨  i≤j+i _ (+ r) ⟩
   + r + q * + d  ≡˘⟨ a≡a%ℕn+[a/ℕn]*n n d ⟩
   n              ∎
 

src/Data/Integer/DivMod.agda

@@ -88,6 +88,8 @@ record NonZero (n : ℕ) : Set where
   field
     nonZero : T (not (n ≡ᵇ 0))
 
+-- Instances
+
 instance
   nonZero : ∀ {n} → NonZero (suc n)
   nonZero = _