[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100419144459
 Ignore-this: 4ff7f5981923cf4de752dde5ad10fe69
] hunk ./README/Nat.agda 31
-  module ℕ = CommutativeSemiring Nat.commutativeSemiring
+  module CS = CommutativeSemiring Nat.commutativeSemiring
hunk ./README/Nat.agda 34
-ex₃ m n = ℕ.*-comm m n
+ex₃ m n = CS.*-comm m n
hunk ./README/Nat.agda 44
-  m * (n + 0)  ≡⟨ cong (_*_ m) (proj₂ ℕ.+-identity n) ⟩
-  m * n        ≡⟨ ℕ.*-comm m n ⟩
+  m * (n + 0)  ≡⟨ cong (_*_ m) (proj₂ CS.+-identity n) ⟩
+  m * n        ≡⟨ CS.*-comm m n ⟩
hunk ./src/Data/Nat/GCD.agda 79
-  -- If m and n have greatest common divisor d, then one of the
-  -- following two equations is satisfied, for some numbers x and y.
-  -- The proof is "lemma" below (Bézout's lemma).
-  --
-  -- (If this identity was stated using integers instead of natural
-  -- numbers, then it would not be necessary to have two equations.)
+  module Identity where
hunk ./src/Data/Nat/GCD.agda 81
-  data Identity (d m n : ℕ) : Set where
-    +- : (x y : ℕ) (eq : d + y * n ≡ x * m) → Identity d m n
-    -+ : (x y : ℕ) (eq : d + x * m ≡ y * n) → Identity d m n
+    -- If m and n have greatest common divisor d, then one of the
+    -- following two equations is satisfied, for some numbers x and y.
+    -- The proof is "lemma" below (Bézout's lemma).
+    --
+    -- (If this identity was stated using integers instead of natural
+    -- numbers, then it would not be necessary to have two equations.)
hunk ./src/Data/Nat/GCD.agda 88
-  module Identity where
+    data Identity (d m n : ℕ) : Set where
+      +- : (x y : ℕ) (eq : d + y * n ≡ x * m) → Identity d m n
+      -+ : (x y : ℕ) (eq : d + x * m ≡ y * n) → Identity d m n
hunk ./src/Data/Nat/GCD.agda 120
-  -- This type packs up the gcd, the proof that it is a gcd, and the
-  -- proof that it satisfies Bézout's identity.
-
-  data Lemma (m n : ℕ) : Set where
-    result : (d : ℕ) (g : GCD m n d) (b : Identity d m n) → Lemma m n
+  open Identity public using (Identity; +-; -+)
hunk ./src/Data/Nat/GCD.agda 124
+    -- This type packs up the gcd, the proof that it is a gcd, and the
+    -- proof that it satisfies Bézout's identity.
+
+    data Lemma (m n : ℕ) : Set where
+      result : (d : ℕ) (g : GCD m n d) (b : Identity d m n) → Lemma m n
+
hunk ./src/Data/Nat/GCD.agda 149
+  open Lemma public using (Lemma; result)
+