From 6f64f2bbba6d5488cc36b8e2f5a717e866a3015d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 11 Jul 2008 16:49:18 +0000 Subject: [PATCH] Exists is no longer an ad-hoc notation hard-coded in the parser. It was so becauses it was previously impossible to declare a notation that changed the level of its subterms. --- helm/software/components/content_pres/cicNotationParser.ml | 4 ---- helm/software/matita/core_notation.moo | 4 ++++ 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index aca53578b..d7da2ff82 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -550,7 +550,6 @@ EXTEND ]; binder: [ [ SYMBOL <:unicode> (* Π *) -> `Pi -(* | SYMBOL <:unicode> |+ ∃ +| -> `Exists *) | SYMBOL <:unicode> (* ∀ *) -> `Forall | SYMBOL <:unicode> (* λ *) -> `Lambda ] @@ -649,9 +648,6 @@ EXTEND [ [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" -> return_term loc (fold_cluster b vars typ body) - | SYMBOL <:unicode> (* ∃ *); - (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19"-> - return_term loc (fold_exists vars typ body) ] ]; term: LEVEL "70" diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 905529317..2ea6f331d 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -4,6 +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) }. + notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. -- 2.39.2