Merge pull request #45 from m0davis/master

use record instead of data for Σ

src/Prelude/Product.agda

@@ -8,19 +8,19 @@ open import Prelude.Decidable
 open import Prelude.Ord
 
 infixr 1 _,_
-data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
-  _,_ : (x : A) (y : B x) → Σ A B
+record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
+  no-eta-equality
+  constructor _,_
+  field
+    fst : A
+    snd : B fst
+
+open Σ public
 
 instance
   ipair : ∀ {a b} {A : Set a} {B : A → Set b} {{x : A}} {{y : B x}} → Σ A B
   ipair {{x}} {{y}} = x , y
 
-fst : ∀ {a b} {A : Set a} {B : A → Set b} → Σ A B → A
-fst (x , y) = x
-
-snd : ∀ {a b} {A : Set a} {B : A → Set b} (p : Σ A B) → B (fst p)
-snd (x , y) = y
-
 infixr 3 _×_
 _×_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
 A × B = Σ A (λ _ → B)

src/Tactic/Reflection/Quote.agda

@@ -29,7 +29,11 @@ unquoteDecl QuotableBool       = deriveQuotable QuotableBool       (quote Bool)
 unquoteDecl QuotableList       = deriveQuotable QuotableList       (quote List)
 unquoteDecl QuotableMaybe      = deriveQuotable QuotableMaybe      (quote Maybe)
 unquoteDecl QuotableEither     = deriveQuotable QuotableEither     (quote Either)
-unquoteDecl QuotableΣ          = deriveQuotable QuotableΣ          (quote Σ)
+
+instance
+  QuotableΣ : ∀ {a b} {A : Set a} {B : A → Set b} {{_ : Quotable A}} {{_ : {x : A} → Quotable (B x)}} → Quotable (Σ A λ a → B a)
+  QuotableΣ = record { ` = λ { (x , y) → con (quote _,_) ((vArg (` x)) ∷ vArg (` y) ∷ [])} }
+
 unquoteDecl Quotable⊤          = deriveQuotable Quotable⊤          (quote ⊤)
 unquoteDecl Quotable⊥          = deriveQuotable Quotable⊥          (quote ⊥)
 unquoteDecl Quotable≡          = deriveQuotable Quotable≡          (quote _≡_)