From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 13 Dec 2011 11:12:02 +0000 (+0000)
Subject: Sig in Prop
X-Git-Tag: make_still_working~2016
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=583977e3d9e646efcaf5b8e956f0407fd3777236;p=helm.git

Sig in Prop
---

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index bfcf7731f..a6749bb39 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -123,6 +123,12 @@ notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
         λ${ident E}.$s ] (refl ? $t) }.
 
+(* Prop sigma *)
+record PSig (A:Type[0]) (P:A→Prop) : Type[0] ≝
+  {elem:>A; eproof: P elem}.
+  
+interpretation "subset type" 'sigma x = (PSig ? x).
+
 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  with precedence 10
 for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒