[Turned Record into a record type.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110622090529
 Ignore-this: 8c3e59f5d1188a10a0f86b33a082a49b
] hunk ./src/Record.agda 63
-  -- Record is a data type to ensure that the signature can be
+  -- Record is a record type to ensure that the signature can be
hunk ./src/Record.agda 66
-  data Record {s} (Sig : Signature s) : Set s where
-    rec : (r : Record-fun Sig) → Record Sig
+  record Record {s} (Sig : Signature s) : Set s where
+    constructor rec
+    field fun : Record-fun Sig
hunk ./src/Record.agda 75
--- A projection function for Record. (Unfortunately Agda as of version
--- 2.2.10 does not allow us to turn Record into a record type.)
-
-rec-fun : ∀ {s} {Sig : Signature s} → Record Sig → Record-fun Sig
-rec-fun (rec r) = r
-
hunk ./src/Record.agda 111
-  Rec⇒Rec′ ∅             r = rec-fun r
-  Rec⇒Rec′ (Sig , ℓ ∶ A) r = (Rec⇒Rec′ _ (Σ.proj₁ r′) , Σ.proj₂ r′)
-                                   where r′ = rec-fun r
-  Rec⇒Rec′ (Sig , ℓ ≔ a) r = (Rec⇒Rec′ _ (Manifest-Σ.proj₁ r′) ,)
-                             where r′ = rec-fun r
+  Rec⇒Rec′ ∅             (rec r) = r
+  Rec⇒Rec′ (Sig , ℓ ∶ A) (rec r) = (Rec⇒Rec′ _ (Σ.proj₁ r) , Σ.proj₂ r)
+  Rec⇒Rec′ (Sig , ℓ ≔ a) (rec r) = (Rec⇒Rec′ _ (Manifest-Σ.proj₁ r) ,)
hunk ./src/Record.agda 181
-_∣_ {Sig = ∅}            r ℓ {}
-_∣_ {Sig = Sig , ℓ′ ∶ A} r ℓ with ℓ ≟ ℓ′
-... | yes _ = Σ.proj₁ (rec-fun r)
-... | no  _ = Σ.proj₁ (rec-fun r) ∣ ℓ
-_∣_ {Sig = Sig , ℓ′ ≔ a} r ℓ with ℓ ≟ ℓ′
-... | yes _ = Manifest-Σ.proj₁ (rec-fun r)
-... | no  _ = Manifest-Σ.proj₁ (rec-fun r) ∣ ℓ
+_∣_ {Sig = ∅}            r       ℓ {}
+_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ with ℓ ≟ ℓ′
+... | yes _ = Σ.proj₁ r
+... | no  _ = Σ.proj₁ r ∣ ℓ
+_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ with ℓ ≟ ℓ′
+... | yes _ = Manifest-Σ.proj₁ r
+... | no  _ = Manifest-Σ.proj₁ r ∣ ℓ
hunk ./src/Record.agda 194
-_·_ {Sig = ∅}            r ℓ {}
-_·_ {Sig = Sig , ℓ′ ∶ A} r ℓ with ℓ ≟ ℓ′
-... | yes _ = Σ.proj₂ (rec-fun r)
-... | no  _ = Σ.proj₁ (rec-fun r) · ℓ
-_·_ {Sig = Sig , ℓ′ ≔ a} r ℓ with ℓ ≟ ℓ′
-... | yes _ = Manifest-Σ.proj₂ (rec-fun r)
-... | no  _ = Manifest-Σ.proj₁ (rec-fun r) · ℓ
+_·_ {Sig = ∅}            r       ℓ {}
+_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ with ℓ ≟ ℓ′
+... | yes _ = Σ.proj₂ r
+... | no  _ = Σ.proj₁ r · ℓ
+_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ with ℓ ≟ ℓ′
+... | yes _ = Manifest-Σ.proj₂ r
+... | no  _ = Manifest-Σ.proj₁ r · ℓ
hunk ./src/Record.agda 225
-  drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} r with ℓ ≟ ℓ′
-  ... | yes _ = rec (proj₁ (rec-fun r) , proj₂ (rec-fun r))
-                where open Manifest-Σ
-  ... | no  _ = rec ( drop-With (Σ.proj₁ (rec-fun r))
-                    , Σ.proj₂ (rec-fun r)
-                    )
-  drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} r with ℓ ≟ ℓ′
-  ... | yes _ = rec (Manifest-Σ.proj₁ (rec-fun r) ,)
-  ... | no  _ = rec (drop-With (Manifest-Σ.proj₁ (rec-fun r)) ,)
+  drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with ℓ ≟ ℓ′
+  ... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
+  ... | no  _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
+  drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with ℓ ≟ ℓ′
+  ... | yes _ = rec (Manifest-Σ.proj₁ r ,)
+  ... | no  _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)