From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 31 Jan 2012 10:09:05 +0000 (+0000)
Subject: Notation for destructuring let-in for triples fixed.
X-Git-Tag: make_still_working~1961
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=464187875cc79b9ad2d415e638250fb949186670;p=helm.git

Notation for destructuring let-in for triples fixed.
---

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 1dcd79b7a..b7a022ad2 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -145,10 +145,10 @@ for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} 
        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
         λ${ident E}.$s ] ] (refl ? $t) }.
 
-notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp 'as' \nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  with precedence 10
-for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
-       match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → $U with [ mk_Prod (${ident xy}:$V) (${ident z}:$Z) ⇒
+       match $xy return λ${ident a}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
         λ${ident E}:$J.$s ] ] ($refl $A $t) }.
 
 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"