From f524a0d716de2bdc0874aace8f82f6289034eccf Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 28 Apr 2009 19:30:21 +0000 Subject: [PATCH] cicNotationUtil: in fresh_name_generator, "\eta" replaced with "eta", which is an identifier cicNotationPp: debug mode turned off logic/cprop_connectives.ma: duplicate lines removed matitaScript: missing "\n\n" added in front of inline output core_notation.moo: the "default" notation directive has a bug. Commented out. --- .../components/acic_content/cicNotationPp.ml | 2 +- .../acic_content/cicNotationUtil.ml | 3 +- helm/software/matita/core_notation.moo | 54 ++++++++++++++++++- .../matita/library/logic/cprop_connectives.ma | 6 --- helm/software/matita/matitaScript.ml | 2 +- 5 files changed, 56 insertions(+), 11 deletions(-) diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index a994c9fd1..45fa23a0d 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -34,7 +34,7 @@ module Env = CicNotationEnv * be added to the output of pp_term. * set to false if you need, for example, cut and paste from matitac output to * matitatop *) -let debug_printing = true +let debug_printing = false let pp_binder = function | `Lambda -> "lambda" diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 48258d7ba..60fe6357d 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -362,7 +362,8 @@ let fresh_id () = !fresh_index (* TODO ensure that names generated by fresh_var do not clash with user's *) -let fresh_name () = "η" ^ string_of_int (fresh_id ()) + (* FG: "η" is not an identifier (it is rendered, but not be parsed) *) +let fresh_name () = "eta" ^ string_of_int (fresh_id ()) let rec freshen_term ?(index = ref 0) term = let freshen_term = freshen_term ~index in diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index fc6a15b06..94b38082b 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -1,28 +1,78 @@ +(* exists *******************************************************************) + +notation < "hvbox(\exists ident i : ty break . p)" + with precedence 20 +for @{'exists (\lambda ${ident i} : $ty. $p) }. + +notation < "hvbox(\exists ident i break . p)" + with precedence 20 +for @{'exists (\lambda ${ident i}. $p) }. + +(* notation < "hvbox(\exists ident i opt (: ty) break . p)" - right associative with precedence 20 + with precedence 20 for @{ 'exists ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. +*) +notation > "\exists list1 ident x sep , : T. term 19 Px" + with precedence 20 +for + @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }. + +notation > "\exists list1 ident x sep , . term 19 Px" + with precedence 20 +for + @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }. + +(* notation > "\exists list1 ident x sep , opt (: T). term 19 Px" with precedence 20 for ${ default @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } } @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } } }. +*) + +(* sigma ********************************************************************) +notation < "hvbox(\Sigma ident i : ty break . p)" + with precedence 20 +for @{'sigma (\lambda ${ident i} : $ty. $p) }. + +notation < "hvbox(\Sigma ident i break . p)" + with precedence 20 +for @{'sigma (\lambda ${ident i}. $p) }. + +(* notation < "hvbox(\Sigma ident i opt (: ty) break . p)" - right associative with precedence 20 + with precedence 20 for @{ 'sigma ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. +*) +notation > "\Sigma list1 ident x sep , : T. term 19 Px" + with precedence 20 +for + @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }. + +notation > "\Sigma list1 ident x sep , . term 19 Px" + with precedence 20 +for + @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }. + +(* notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px" with precedence 20 for ${ default @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } } @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } } }. +*) + +(* other notations **********************************************************) notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma index 31cd9c576..2a5af4406 100644 --- a/helm/software/matita/library/logic/cprop_connectives.ma +++ b/helm/software/matita/library/logic/cprop_connectives.ma @@ -75,11 +75,6 @@ interpretation "logical iff type1" 'iff1 x y = (Iff1 x y). inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. - -notation "\ll term 19 a, break term 19 b \gg" -with precedence 90 for @{'dependent_pair $a $b}. -interpretation "dependent pair" 'dependent_pair a b = - (ex_introT _ _ a b). interpretation "CProp exists" 'exists \eta.x = (exT _ x). @@ -88,7 +83,6 @@ with precedence 90 for @{'dependent_pair $a $b}. interpretation "dependent pair" 'dependent_pair a b = (ex_introT _ _ a b). - definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x]. definition pi2exT ≝ λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p]. diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index a941bf088..9fb92c274 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -569,7 +569,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) | TA.Inline (_,style,suri,prefix,flavour) -> - let str = + let str = "\n\n" ^ ApplyTransformation.txt_of_inline_macro ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") -- 2.39.2