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.
* be added to the output of pp_term.
* set to false if you need, for example, cut and paste from matitac output to
* matitatop *)
* 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"
let pp_binder = function
| `Lambda -> "lambda"
!fresh_index
(* TODO ensure that names generated by fresh_var do not clash with user's *)
!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
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
+(* 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)"
notation < "hvbox(\exists ident i opt (: ty) break . p)"
- right associative with precedence 20
for @{ 'exists ${default
@{\lambda ${ident i} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
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)} } }
}.
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)"
notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
- right associative with precedence 20
for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
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)} } }
}.
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}.
notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
with precedence 90 for @{ 'pair $a $b}.
inductive exT (A:Type) (P:A→CProp) : CProp ≝
ex_introT: ∀w:A. P w → exT A P.
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).
interpretation "CProp exists" 'exists \eta.x = (exT _ x).
interpretation "dependent pair" 'dependent_pair a b =
(ex_introT _ _ 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].
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].
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
| TA.Inline (_,style,suri,prefix,flavour) ->
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
| TA.Inline (_,style,suri,prefix,flavour) ->
ApplyTransformation.txt_of_inline_macro
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
ApplyTransformation.txt_of_inline_macro
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")