From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 Dec 2011 15:10:12 +0000 (+0000)
Subject: Dependent pairs (i.e. Sigma types in Type[0]) are back, but are not the default
X-Git-Tag: make_still_working~2008
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc35589f8448d6a7bd803992e918acc7b720e7fb;p=helm.git

Dependent pairs (i.e. Sigma types in Type[0]) are back, but are not the default
ones.
---

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 348bf92de..1d3883048 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -55,6 +55,19 @@ lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. 
 | #a #H #p normalize @p @refl
 ] qed.
 
+(* dependent pair *)
+record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+    dpi1: A
+  ; dpi2: f dpi1
+  }.
+
+interpretation "DPair" 'sigma x = (DPair ? x).
+
+notation "hvbox(« term 19 a, break term 19 b»)" 
+with precedence 90 for @{ 'dp $a $b }.
+
+interpretation "mk_DPair" 'dp x y = (mk_DPair ?? x y).
+
 (* sigma *)
 record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
     pi1: A
@@ -63,9 +76,6 @@ record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
   
 interpretation "Sigma" 'sigma x = (Sig ? x).
 
-notation "hvbox(« term 19 a, break term 19 b»)" 
-with precedence 90 for @{ 'dp $a $b }.
-
 interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
 
 (* Prod *)