From e6d21d40633603dab229f94ff6becbd509eb6df9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 12 Jul 2008 11:17:17 +0000 Subject: [PATCH] Notation for existential partially fixed: it is now possible to write \exists a,b,c:T.P (possibly omitting the type). In any case, however, the type is got rid of during parsing. --- helm/software/matita/core_notation.moo | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 2ea6f331d..c7f1e5021 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -4,9 +4,10 @@ for @{ 'exists ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. -notation > "\exists ident x:A.break term 19 Px" with precedence 20 for @{ 'exists (λ${ident x}:$A.$Px) }. - -notation > "\exists ident x.break term 19 Px" with precedence 20 for @{ 'exists (λ${ident x}.$Px) }. +(* Bugged notation: $T is not used if provided *) +notation > "\exists list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 + for ${fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)}}. notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. -- 2.39.2