[ re #192 ] Make _|_ a record (#196)

Author: gallais

CHANGELOG.md

@@ -49,6 +49,10 @@ Non-backwards compatible changes
 * Moved `Data.Vec.Equality` to `Data.Vec.Relation.Equality` (see "Deprecated
   features" section for explanation)
 
+* Changed Data.Nat.Divisibility's `_|_` from data to record. As a consequence,
+  the two parameters are not implicit arguments of the constructor anymore (but
+  such values can be destructed using a let-binding rather than a with-clause).
+
 Deprecated features
 -------------------
 

src/Data/Nat/Divisibility.agda

@@ -30,8 +30,10 @@ open import Function
 
 infix 4 _∣_ _∤_
 
-data _∣_ : ℕ → ℕ → Set where
-  divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n
+record _∣_ (m n : ℕ) : Set where
+  constructor divides
+  field quotient : ℕ
+        equality : n ≡ quotient * m
 
 _∤_ : Rel ℕ _
 m ∤ n = ¬ (m ∣ n)
@@ -61,11 +63,10 @@ quotient (divides q _) = q
   divides (q * p) (sym (*-assoc q p _))
 
 ∣-antisym : Antisymmetric _≡_ _∣_
-∣-antisym (divides {n = zero} _ _) (divides q refl) = *-comm q 0
-∣-antisym (divides p eq) (divides {n = zero} _ _) =
-  trans (*-comm 0 p) (sym eq)
-∣-antisym (divides {n = suc _} p eq₁) (divides {n = suc _} q eq₂) =
-    ≤-antisym (∣⇒≤ (divides p eq₁)) (∣⇒≤ (divides q eq₂))
+∣-antisym {m} {0} _ (divides q eq) = trans eq (*-comm q 0)
+∣-antisym {0} {n} (divides p eq) _ = sym (trans eq (*-comm p 0))
+∣-antisym {suc m} {suc n} (divides p eq₁) (divides q eq₂) =
+  ≤-antisym (∣⇒≤ (divides p eq₁)) (∣⇒≤ (divides q eq₂))
 
 ∣-isPreorder : IsPreorder _≡_ _∣_
 ∣-isPreorder = record