From: Ferruccio Guidi Date: Fri, 17 Nov 2006 18:20:47 +0000 (+0000) Subject: helm_registry: added the pair unmarshaller X-Git-Tag: make_still_working~6659 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;hp=bb691187f8bbe22ec37ca41f9f3f42f9d8e505df;p=helm.git helm_registry: added the pair unmarshaller grafiteAstPp: bug-fixed transcript: coercion handling improved CoRN-Decl: regenerated accordingly --ehis line, and those below, will be ignored-- M software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma M software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma M software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma M software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma M software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma M software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma M software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma M software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma M software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma M software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma M software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma M software/matita/contribs/CoRN-Decl/model/rings/Zring.ma M software/matita/contribs/CoRN-Decl/model/rings/Qring.ma M software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma M software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma M software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma M software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma M software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma M software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma M software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma M software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma M software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma M software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma M software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma M software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma M software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma M software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma M software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma M software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma M software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma M software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma M software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma M software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma M software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma M software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma M software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma M software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma M software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma M software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma M software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma M software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma M software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma M software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma M software/matita/contribs/CoRN-Decl/metrics/Equiv.ma M software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma M software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma M software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma M software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma M software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma M software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma M software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma M software/matita/contribs/CoRN-Decl/reals/CReals1.ma M software/matita/contribs/CoRN-Decl/reals/Series.ma M software/matita/contribs/CoRN-Decl/reals/NRootIR.ma M software/matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma M software/matita/contribs/CoRN-Decl/reals/IVT.ma M software/matita/contribs/CoRN-Decl/reals/RealLists.ma M software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma M software/matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma M software/matita/contribs/CoRN-Decl/reals/RealFuncts.ma M software/matita/contribs/CoRN-Decl/reals/Intervals.ma M software/matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma M software/matita/contribs/CoRN-Decl/reals/CReals.ma M software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma M software/matita/contribs/CoRN-Decl/reals/Q_dense.ma M software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma M software/matita/contribs/CoRN-Decl/reals/R_morphism.ma M software/matita/contribs/CoRN-Decl/reals/CSumsReals.ma M software/matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma M software/matita/contribs/CoRN-Decl/complex/NRootCC.ma M software/matita/contribs/CoRN-Decl/complex/CComplex.ma M software/matita/contribs/CoRN-Decl/complex/AbsCC.ma M software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma D software/matita/contribs/CoRN-Decl/CoRN_notation.ma M software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma M software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma M software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma M software/matita/contribs/CoRN-Decl/fta/CC_Props.ma M software/matita/contribs/CoRN-Decl/fta/FTAreg.ma M software/matita/contribs/CoRN-Decl/fta/FTA.ma M software/matita/contribs/CoRN-Decl/fta/MainLemma.ma M software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma M software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma M software/matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma M software/matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma M software/matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma M software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma M software/matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma M software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma M software/matita/contribs/CoRN-Decl/tactics/Step.ma M software/matita/contribs/CoRN-Decl/tactics/AlgReflection.ma M software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma M software/matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma M software/matita/contribs/CoRN-Decl/transc/RealPowers.ma M software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma M software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma M software/matita/contribs/CoRN-Decl/transc/Exponential.ma M software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma M software/matita/contribs/CoRN-Decl/transc/Pi.ma M software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma M software/matita/contribs/CoRN-Decl/transc/SinCos.ma M software/matita/contribs/CoRN-Decl/transc/TrigMon.ma M software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma M software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma M software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma M software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma M software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma M software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma M software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma M software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma M software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma M software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma M software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma M software/matita/contribs/CoRN-Decl/ftc/Partitions.ma M software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma M software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma M software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma M software/matita/contribs/CoRN-Decl/ftc/Derivative.ma M software/matita/contribs/CoRN-Decl/ftc/Composition.ma M software/matita/contribs/CoRN-Decl/ftc/Integral.ma M software/matita/contribs/CoRN-Decl/ftc/Continuity.ma M software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma M software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma M software/matita/contribs/CoRN-Decl/ftc/Taylor.ma M software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma M software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma M software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma M software/matita/contribs/CoRN-Decl/ftc/FTC.ma M software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma M software/matita/contribs/CoRN-Decl/ftc/Rolle.ma M software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma M software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma M software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma M software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma M software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma M software/matita/contribs/CoRN-Decl/algebra/CRings.ma M software/matita/contribs/CoRN-Decl/algebra/Expon.ma M software/matita/contribs/CoRN-Decl/algebra/CSums.ma M software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma M software/matita/contribs/CoRN-Decl/algebra/CLogic.ma M software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma M software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma M software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma M software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma M software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma M software/matita/contribs/CoRN-Decl/algebra/Basics.ma M software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma M software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma M software/matita/contribs/CoRN-Decl/algebra/CFields.ma M software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma M software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma M software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma M software/matita/contribs/CoRN-Decl/algebra/ListType.ma M software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma M software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma M software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma M software/matita/contribs/CoRN-Decl/algebra/CGroups.ma A software/matita/contribs/CoRN-Decl/CoRN.ma M software/components/grafite/grafiteAstPp.ml M software/components/binaries/transcript/CoRN.conf.xml M software/components/binaries/transcript/grafite.ml M software/components/binaries/transcript/v8Parser.mly M software/components/binaries/transcript/types.ml M software/components/binaries/transcript/engine.ml M software/components/registry/helm_registry.ml M software/components/registry/helm_registry.mli --- diff --git a/helm/software/components/binaries/transcript/CoRN.conf.xml b/helm/software/components/binaries/transcript/CoRN.conf.xml index 6be3a5634..ad576e986 100644 --- a/helm/software/components/binaries/transcript/CoRN.conf.xml +++ b/helm/software/components/binaries/transcript/CoRN.conf.xml @@ -1,11 +1,13 @@
- CoRN + CoRN + CoRN-Decl cic:/CoRN cic:/matita/CoRN-Decl /projects/helm/exportation/CoRN $(transcript.helm_dir)/matita/contribs/CoRN-Decl .v + Z_of_nat cic:/Coq/ZArith/BinInt
diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 62fcf03df..3b1e8d773 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -37,12 +37,14 @@ type status = { helm_dir: string; heading_path: string; heading_lines: int; - package: string; + input_package: string; + output_package: string; input_base_uri: string; output_base_uri: string; input_path: string; output_path: string; script_ext: string; + coercions: (string * string) list; files: string list; requires: (string * string) list; scripts: script array @@ -87,17 +89,21 @@ let init () = load_registry default_registry let make registry = + let id x = x in + let get_coercions = R.get_list (R.pair id id) in load_registry registry; let st = { helm_dir = R.get_string "transcript.helm_dir"; heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; - package = R.get_string "package.name"; + input_package = R.get_string "package.input_name"; + output_package = R.get_string "package.output_name"; input_base_uri = R.get_string "package.input_base_uri"; output_base_uri = R.get_string "package.output_base_uri"; input_path = R.get_string "package.input_path"; output_path = R.get_string "package.output_path"; script_ext = R.get_string "package.script_type"; + coercions = get_coercions "package.coercion"; files = []; requires = []; scripts = Array.make default_scripts default_script @@ -133,7 +139,10 @@ let set_baseuri st name = let require st name inc = set_items st name [T.Include inc] - + +let get_coercion st str = + try List.assoc str st.coercions with Not_found -> "" + let commit st name = let i = get_index st name in let script = st.scripts.(i) in @@ -147,28 +156,33 @@ let commit st name = st.scripts.(i) <- default_script let produce st = - let notation = st.package ^ "_notation" in let init name = set_heading st name; set_baseuri st name in let partition = function - | T.Notation _ -> false - | _ -> true + | T.Coercion (false, _) + | T.Notation (false, _) -> false + | _ -> true in let produce st name = let in_base_uri = Filename.concat st.input_base_uri name in let out_base_uri = Filename.concat st.output_base_uri name in let filter = function - | T.Inline (k, obj) -> + | T.Inline (k, obj) -> let s = obj ^ G.string_of_inline_kind k in Some (T.Inline (k, Filename.concat in_base_uri s)) - | T.Include s -> + | T.Include s -> begin try Some (T.Include (List.assoc s st.requires)) with Not_found -> None end - | T.Coercion obj -> + | T.Coercion (b, obj) -> + let str = get_coercion st obj in + let base_uri = + if str <> "" then str else + if b then out_base_uri else in_base_uri + in let s = obj ^ G.string_of_inline_kind T.Con in - Some (T.Coercion (Filename.concat out_base_uri s)) - | item -> Some item + Some (T.Coercion (b, Filename.concat base_uri s)) + | item -> Some item in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; let file = Filename.concat st.input_path (name ^ st.script_ext) in @@ -181,10 +195,12 @@ let produce st = let local_items, global_items = List.partition partition items in let comment = T.Line (Printf.sprintf "From %s" name) in if global_items <> [] then - set_items st notation (comment :: global_items); - init name; require st name notation; + set_items st st.input_package (comment :: global_items); + init name; require st name st.input_package; set_items st name local_items; commit st name with e -> prerr_endline (Printexc.to_string e); close_in ich in - init notation; List.iter (produce st) st.files; commit st notation + init st.input_package; + List.iter (produce st) st.files; + commit st st.input_package diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 86a95270a..dcc6b9fb1 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -90,8 +90,8 @@ let commit och items = | T.Line line -> out_line_comment och line | T.BaseUri uri -> out_command och (set "baseuri" uri) | T.Include script -> out_command och (require script) - | T.Coercion uri -> out_command och (coercion uri) - | T.Notation notation -> out_unexported och "NOTATION" notation (**) + | T.Coercion specs -> out_command och (coercion (snd specs)) + | T.Notation specs -> out_unexported och "NOTATION" (snd specs) (**) | T.Inline specs -> out_command och (inline (snd specs)) | T.Comment comment -> out_comment och comment | T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index e51122b3f..73420ee59 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +type local = bool + type inline_kind = Con | Ind | Var type item = Heading of (string * int) @@ -31,8 +33,8 @@ type item = Heading of (string * int) | Unexport of string | BaseUri of string | Include of string - | Coercion of string - | Notation of string + | Coercion of (local * string) + | Notation of (local * string) | Inline of (inline_kind * string) | Verbatim of string | Discard of string diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly index 61413e7fe..06d4d908b 100644 --- a/helm/software/components/binaries/transcript/v8Parser.mly +++ b/helm/software/components/binaries/transcript/v8Parser.mly @@ -43,6 +43,12 @@ let strip1 s = String.sub s 1 (String.length s - 1) + + let coercion str = + [T.Coercion (false, str); T.Coercion (true, str)] + + let notation str = + [T.Notation (false, str); T.Notation (true, str)] %} %token SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC %token LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC @@ -189,9 +195,9 @@ ; field: | ident cn unexports_r - { $1 ^ $2 ^ fst $3, snd $3 } + { $1 ^ $2 ^ fst $3, snd $3 } | ident coe unexports_r - { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion (trim $1)] } + { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) } ; fields: | field { $1 } @@ -269,9 +275,9 @@ | load str FS { out "REQ" $2; [T.Include (strip2 (trim $2))] } | coerc qid spcs cn unexports FS - { out "COERCE" (hd $2); [T.Coercion (hd $2)] } + { out "COERCE" (hd $2); coercion (hd $2) } | id coerc qid spcs cn unexports FS - { out "COERCE" (hd $3); [T.Coercion (hd $3)] } + { out "COERCE" (hd $3); coercion (hd $3) } | th ident error { out "ERROR" $2; failwith ("macro_step " ^ $2) } | ind ident error @@ -284,7 +290,7 @@ | OQ verbatims CQ { [T.Comment $2] } | macro_step { $1 } | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ trim $3)] } + | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) } | error { out "ERROR" "item"; failwith "item" } ; items: diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index d064ef619..2e3d95abe 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -222,7 +222,7 @@ let pp_default what uris = (String.concat " " (List.map UriManager.string_of_uri uris)) let pp_coercion uri do_composites arity = - sprintf "coercion \"%s\" %d (* %s *)" (UriManager.string_of_uri uri) arity + sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity (if do_composites then "compounds" else "no compounds") let pp_command ~term_pp ~obj_pp = function diff --git a/helm/software/components/registry/helm_registry.ml b/helm/software/components/registry/helm_registry.ml index b7b3de11d..3753232b6 100644 --- a/helm/software/components/registry/helm_registry.ml +++ b/helm/software/components/registry/helm_registry.ml @@ -109,6 +109,12 @@ let of_int = handle_type_error string_of_int let of_float = handle_type_error string_of_float let of_bool = handle_type_error string_of_bool +(* FG *) +let pair fst_unmarshaller snd_unmarshaller v = + match Str.split spaces_rex v with + | [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd + | _ -> raise (Type_error "not a pair") + (* escapes for xml configuration file *) let (escape, unescape) = let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in @@ -198,11 +204,9 @@ let get_list registry unmarshaller key = List.map unmarshaller (get registry key) with Key_not_found _ -> [] -let get_pair registry fst_unmarshaller snd_unmarshaller key = - let v = singleton (get registry key) in - match Str.split spaces_rex v with - | [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd - | _ -> raise (Type_error "not a pair") +(* FG *) +let get_pair registry fst_unmarshaller snd_unmarshaller = + get_typed registry (pair fst_unmarshaller snd_unmarshaller) let set_list registry marshaller ~key ~value = Hashtbl.remove registry key; diff --git a/helm/software/components/registry/helm_registry.mli b/helm/software/components/registry/helm_registry.mli index 1ef1aa3b7..77c6f6cc3 100644 --- a/helm/software/components/registry/helm_registry.mli +++ b/helm/software/components/registry/helm_registry.mli @@ -132,6 +132,7 @@ val string: string -> string val int: string -> int val float: string -> float val bool: string -> bool +val pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b (** {3 Typed getters} *) diff --git a/helm/software/matita/contribs/CoRN-Decl/CoRN.ma b/helm/software/matita/contribs/CoRN-Decl/CoRN.ma new file mode 100644 index 000000000..6a0b5b4f3 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Decl/CoRN.ma @@ -0,0 +1,731 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/CoRN-Decl/CoRN". + +(* From algebra/Basics ****************************************************) + +(* NOTATION +Notation Pair := (pair (B:=_)). +*) + +(* NOTATION +Notation Proj1 := (proj1 (B:=_)). +*) + +(* NOTATION +Notation Proj2 := (proj2 (B:=_)). +*) + +coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *). + +(* From algebra/CAbGroups *************************************************) + +coercion cic:/CoRN/algebra/CAbGroups/cag_crr.con 0 (* compounds *). + +(* From algebra/CAbMonoids ************************************************) + +coercion cic:/CoRN/algebra/CAbMonoids/cam_crr.con 0 (* compounds *). + +(* From algebra/CFields ***************************************************) + +coercion cic:/CoRN/algebra/CFields/cf_crr.con 0 (* compounds *). + +(* NOTATION +Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80). +*) + +(* NOTATION +Notation "{1/} x" := (Frecip x) (at level 2, right associativity). +*) + +(* NOTATION +Infix "{/}" := Fdiv (at level 41, no associativity). +*) + +(* From algebra/CGroups ***************************************************) + +coercion cic:/CoRN/algebra/CGroups/cg_crr.con 0 (* compounds *). + +(* NOTATION +Notation "[--] x" := (cg_inv x) (at level 2, right associativity). +*) + +(* NOTATION +Infix "[-]" := cg_minus (at level 50, left associativity). +*) + +(* NOTATION +Notation "{--} x" := (Finv x) (at level 2, right associativity). +*) + +(* NOTATION +Infix "{-}" := Fminus (at level 50, left associativity). +*) + +(* From algebra/CLogic ****************************************************) + +(* NOTATION +Infix "IFF" := Iff (at level 60, right associativity). +*) + +(* NOTATION +Infix "or" := COr (at level 85, right associativity). +*) + +(* NOTATION +Infix "and" := CAnd (at level 80, right associativity). +*) + +(* NOTATION +Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp) + (at level 0, x at level 99) : type_scope. +*) + +(* NOTATION +Notation "{ x : A | P | Q }" := + (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) : + type_scope. +*) + +(* NOTATION +Notation ProjT1 := (proj1_sigT _ _). +*) + +(* NOTATION +Notation ProjT2 := (proj2_sigT _ _). +*) + +(* From algebra/CMonoids **************************************************) + +coercion cic:/CoRN/algebra/CMonoids/cm_crr.con 0 (* compounds *). + +(* NOTATION +Notation Zero := (cm_unit _). +*) + +(* From algebra/COrdAbs ***************************************************) + +(* NOTATION +Notation ZeroR := (Zero:R). +*) + +(* NOTATION +Notation AbsBig := (absBig _). +*) + +(* From algebra/COrdCauchy ************************************************) + +coercion cic:/CoRN/algebra/COrdCauchy/CS_seq.con 0 (* compounds *). + +(* From algebra/COrdFields ************************************************) + +coercion cic:/CoRN/algebra/COrdFields/cof_crr.con 0 (* compounds *). + +(* NOTATION +Infix "[<]" := cof_less (at level 70, no associativity). +*) + +(* NOTATION +Infix "[>]" := greater (at level 70, no associativity). +*) + +(* NOTATION +Infix "[<=]" := leEq (at level 70, no associativity). +*) + +(* NOTATION +Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20). +*) + +(* From algebra/COrdFields2 ***********************************************) + +(* NOTATION +Notation ZeroR := (Zero:R). +*) + +(* NOTATION +Notation OneR := (One:R). +*) + +(* From algebra/CPoly_ApZero **********************************************) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* From algebra/CPoly_Degree **********************************************) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* NOTATION +Notation FX := (cpoly_cring F). +*) + +(* From algebra/CPoly_NthCoeff ********************************************) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* From algebra/CPolynomials **********************************************) + +(* NOTATION +Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity). +*) + +(* NOTATION +Notation RX := (cpoly_cring CR). +*) + +(* NOTATION +Infix "!" := cpoly_apply_fun (at level 1, no associativity). +*) + +(* NOTATION +Notation RX := (cpoly_cring R). +*) + +(* NOTATION +Notation Cpoly := (cpoly CR). +*) + +(* NOTATION +Notation Cpoly_zero := (cpoly_zero CR). +*) + +(* NOTATION +Notation Cpoly_linear := (cpoly_linear CR). +*) + +(* NOTATION +Notation Cpoly_cring := (cpoly_cring CR). +*) + +(* From algebra/CRings ****************************************************) + +coercion cic:/CoRN/algebra/CRings/cr_crr.con 0 (* compounds *). + +(* NOTATION +Notation One := (cr_one _). +*) + +(* NOTATION +Infix "[*]" := cr_mult (at level 40, left associativity). +*) + +(* NOTATION +Notation "x [^] n" := (nexp_op _ n x) (at level 20). +*) + +(* NOTATION +Notation Two := (nring 2). +*) + +(* NOTATION +Notation Three := (nring 3). +*) + +(* NOTATION +Notation Four := (nring 4). +*) + +(* NOTATION +Notation Six := (nring 6). +*) + +(* NOTATION +Notation Eight := (nring 8). +*) + +(* NOTATION +Notation Twelve := (nring 12). +*) + +(* NOTATION +Notation Sixteen := (nring 16). +*) + +(* NOTATION +Notation Nine := (nring 9). +*) + +(* NOTATION +Notation Eighteen := (nring 18). +*) + +(* NOTATION +Notation TwentyFour := (nring 24). +*) + +(* NOTATION +Notation FortyEight := (nring 48). +*) + +(* NOTATION +Infix "{*}" := Fmult (at level 40, left associativity). +*) + +(* NOTATION +Infix "{**}" := Fscalmult (at level 40, left associativity). +*) + +(* NOTATION +Infix "{^}" := Fnth (at level 30, right associativity). +*) + +(* From algebra/CSemiGroups ***********************************************) + +coercion cic:/CoRN/algebra/CSemiGroups/csg_crr.con 0 (* compounds *). + +(* NOTATION +Infix "[+]" := csg_op (at level 50, left associativity). +*) + +(* NOTATION +Infix "{+}" := Fplus (at level 50, left associativity). +*) + +(* From algebra/CSetoidFun ************************************************) + +(* NOTATION +Notation Conj := (conjP _). +*) + +coercion cic:/CoRN/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *). + +(* NOTATION +Notation BDom := (bpfdom _ _). +*) + +coercion cic:/CoRN/algebra/CSetoidFun/pfpfun.con 0 (* compounds *). + +(* NOTATION +Notation Dom := (pfdom _). +*) + +(* NOTATION +Notation Part := (pfpfun _). +*) + +(* NOTATION +Notation "[-C-] x" := (Fconst x) (at level 2, right associativity). +*) + +(* NOTATION +Notation FId := (Fid _). +*) + +(* NOTATION +Infix "[o]" := Fcomp (at level 65, no associativity). +*) + +(* NOTATION +Notation Prj1 := (prj1 _ _ _ _). +*) + +(* NOTATION +Notation Prj2 := (prj2 _ _ _ _). +*) + +(* From algebra/CSetoids **************************************************) + +coercion cic:/CoRN/algebra/CSetoids/cs_crr.con 0 (* compounds *). + +(* NOTATION +Infix "[=]" := cs_eq (at level 70, no associativity). +*) + +(* NOTATION +Infix "[#]" := cs_ap (at level 70, no associativity). +*) + +(* NOTATION +Infix "[~=]" := cs_neq (at level 70, no associativity). +*) + +coercion cic:/CoRN/algebra/CSetoids/csp_pred.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/csp'_pred.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/csr_rel.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/csf_fun.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/csbf_fun.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/un_op_fun.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *). + +coercion cic:/CoRN/algebra/CSetoids/scs_elem.con 0 (* compounds *). + +(* From algebra/CVectorSpace **********************************************) + +coercion cic:/CoRN/algebra/CVectorSpace/vs_vs.con 0 (* compounds *). + +(* NOTATION +Infix "[']" := vs_op (at level 30, no associativity). +*) + +(* From algebra/Expon *****************************************************) + +(* NOTATION +Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0). +*) + +(* From complex/CComplex **************************************************) + +(* NOTATION +Notation CCX := (cpoly_cring CC). +*) + +(* NOTATION +Infix "[+I*]" := cc_set_CC (at level 48, no associativity). +*) + +(* From fta/CC_Props ******************************************************) + +coercion cic:/CoRN/fta/CC_Props/CC_seq.con 0 (* compounds *). + +(* From fta/FTAreg ********************************************************) + +coercion cic:/CoRN/fta/FTAreg/z_el.con 0 (* compounds *). + +coercion cic:/CoRN/fta/FTAreg/Kntup.con 0 (* compounds *). + +(* From ftc/FTC ***********************************************************) + +(* NOTATION +Notation "[-S-] F" := (Fprim F) (at level 20). +*) + +(* From ftc/Integral ******************************************************) + +(* NOTATION +Notation Integral := (integral _ _ Hab). +*) + +(* From ftc/MoreIntervals *************************************************) + +coercion cic:/CoRN/ftc/MoreIntervals/iprop.con 0 (* compounds *). + +(* From ftc/Partitions ****************************************************) + +coercion cic:/CoRN/ftc/Partitions/Pts.con 0 (* compounds *). + +(* From ftc/RefLemma ******************************************************) + +(* NOTATION +Notation g := RL_g. +*) + +(* NOTATION +Notation h := RL_h. +*) + +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)). +*) + +(* NOTATION +Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)). +*) + +(* NOTATION +Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)). +*) + +(* From ftc/RefSeparated **************************************************) + +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). +*) + +(* NOTATION +Notation just2 := + (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)). +*) + +(* From ftc/RefSeparating *************************************************) + +(* NOTATION +Notation m := RS'_m. +*) + +(* NOTATION +Notation h := RS'_h. +*) + +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). +*) + +(* NOTATION +Notation just2 := + (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)). +*) + +(* From ftc/Rolle *********************************************************) + +(* NOTATION +Notation cp := (compact_part a b Hab' d Hd). +*) + +(* From ftc/TaylorLemma ***************************************************) + +(* NOTATION +Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a). +*) + +(* NOTATION +Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b). +*) + +(* From ftc/WeakIVT *******************************************************) + +(* NOTATION +Infix "**" := prodT (at level 20). +*) + +(* From metrics/CMetricSpaces *********************************************) + +coercion cic:/CoRN/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *). + +(* From metrics/CPseudoMSpaces ********************************************) + +coercion cic:/CoRN/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *). + +(* NOTATION +Infix "[-d]" := cms_d (at level 68, left associativity). +*) + +(* From model/structures/Nsec *********************************************) + +(* NOTATION +Infix "{#N}" := ap_nat (no associativity, at level 90). +*) + +(* From model/structures/Qsec *********************************************) + +(* NOTATION +Infix "{=Q}" := Qeq (no associativity, at level 90). +*) + +(* NOTATION +Infix "{#Q}" := Qap (no associativity, at level 90). +*) + +(* NOTATION +Infix "{ P):CProp) - (at level 0, x at level 99) : type_scope. -*) - -(* NOTATION -Notation "{ x : A | P | Q }" := - (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) : - type_scope. -*) - -(* NOTATION -Notation ProjT1 := (proj1_sigT _ _). -*) - -(* NOTATION -Notation ProjT2 := (proj2_sigT _ _). -*) - -(* From algebra/CMonoids **************************************************) - -(* NOTATION -Notation Zero := (cm_unit _). -*) - -(* From algebra/COrdAbs ***************************************************) - -(* NOTATION -Notation ZeroR := (Zero:R). -*) - -(* NOTATION -Notation AbsBig := (absBig _). -*) - -(* From algebra/COrdFields ************************************************) - -(* NOTATION -Infix "[<]" := cof_less (at level 70, no associativity). -*) - -(* NOTATION -Infix "[>]" := greater (at level 70, no associativity). -*) - -(* NOTATION -Infix "[<=]" := leEq (at level 70, no associativity). -*) - -(* NOTATION -Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20). -*) - -(* NOTATION -Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20). -*) - -(* From algebra/COrdFields2 ***********************************************) - -(* NOTATION -Notation ZeroR := (Zero:R). -*) - -(* NOTATION -Notation OneR := (One:R). -*) - -(* From algebra/CPoly_ApZero **********************************************) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* From algebra/CPoly_Degree **********************************************) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation FX := (cpoly_cring F). -*) - -(* From algebra/CPoly_NthCoeff ********************************************) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* From algebra/CPolynomials **********************************************) - -(* NOTATION -Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity). -*) - -(* NOTATION -Notation RX := (cpoly_cring CR). -*) - -(* NOTATION -Infix "!" := cpoly_apply_fun (at level 1, no associativity). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation Cpoly := (cpoly CR). -*) - -(* NOTATION -Notation Cpoly_zero := (cpoly_zero CR). -*) - -(* NOTATION -Notation Cpoly_linear := (cpoly_linear CR). -*) - -(* NOTATION -Notation Cpoly_cring := (cpoly_cring CR). -*) - -(* From algebra/CRings ****************************************************) - -(* NOTATION -Notation One := (cr_one _). -*) - -(* NOTATION -Infix "[*]" := cr_mult (at level 40, left associativity). -*) - -(* NOTATION -Notation "x [^] n" := (nexp_op _ n x) (at level 20). -*) - -(* NOTATION -Notation Two := (nring 2). -*) - -(* NOTATION -Notation Three := (nring 3). -*) - -(* NOTATION -Notation Four := (nring 4). -*) - -(* NOTATION -Notation Six := (nring 6). -*) - -(* NOTATION -Notation Eight := (nring 8). -*) - -(* NOTATION -Notation Twelve := (nring 12). -*) - -(* NOTATION -Notation Sixteen := (nring 16). -*) - -(* NOTATION -Notation Nine := (nring 9). -*) - -(* NOTATION -Notation Eighteen := (nring 18). -*) - -(* NOTATION -Notation TwentyFour := (nring 24). -*) - -(* NOTATION -Notation FortyEight := (nring 48). -*) - -(* NOTATION -Infix "{*}" := Fmult (at level 40, left associativity). -*) - -(* NOTATION -Infix "{**}" := Fscalmult (at level 40, left associativity). -*) - -(* NOTATION -Infix "{^}" := Fnth (at level 30, right associativity). -*) - -(* From algebra/CSemiGroups ***********************************************) - -(* NOTATION -Infix "[+]" := csg_op (at level 50, left associativity). -*) - -(* NOTATION -Infix "{+}" := Fplus (at level 50, left associativity). -*) - -(* From algebra/CSetoidFun ************************************************) - -(* NOTATION -Notation Conj := (conjP _). -*) - -(* NOTATION -Notation BDom := (bpfdom _ _). -*) - -(* NOTATION -Notation Dom := (pfdom _). -*) - -(* NOTATION -Notation Part := (pfpfun _). -*) - -(* NOTATION -Notation "[-C-] x" := (Fconst x) (at level 2, right associativity). -*) - -(* NOTATION -Notation FId := (Fid _). -*) - -(* NOTATION -Infix "[o]" := Fcomp (at level 65, no associativity). -*) - -(* NOTATION -Notation Prj1 := (prj1 _ _ _ _). -*) - -(* NOTATION -Notation Prj2 := (prj2 _ _ _ _). -*) - -(* From algebra/CSetoids **************************************************) - -(* NOTATION -Infix "[=]" := cs_eq (at level 70, no associativity). -*) - -(* NOTATION -Infix "[#]" := cs_ap (at level 70, no associativity). -*) - -(* NOTATION -Infix "[~=]" := cs_neq (at level 70, no associativity). -*) - -(* From algebra/CVectorSpace **********************************************) - -(* NOTATION -Infix "[']" := vs_op (at level 30, no associativity). -*) - -(* From algebra/Expon *****************************************************) - -(* NOTATION -Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0). -*) - -(* From complex/CComplex **************************************************) - -(* NOTATION -Notation CCX := (cpoly_cring CC). -*) - -(* NOTATION -Infix "[+I*]" := cc_set_CC (at level 48, no associativity). -*) - -(* From ftc/FTC ***********************************************************) - -(* NOTATION -Notation "[-S-] F" := (Fprim F) (at level 20). -*) - -(* From ftc/Integral ******************************************************) - -(* NOTATION -Notation Integral := (integral _ _ Hab). -*) - -(* From ftc/RefLemma ******************************************************) - -(* NOTATION -Notation g := RL_g. -*) - -(* NOTATION -Notation h := RL_h. -*) - -(* NOTATION -Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)). -*) - -(* NOTATION -Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)). -*) - -(* NOTATION -Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)). -*) - -(* From ftc/RefSeparated **************************************************) - -(* NOTATION -Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). -*) - -(* NOTATION -Notation just2 := - (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)). -*) - -(* From ftc/RefSeparating *************************************************) - -(* NOTATION -Notation m := RS'_m. -*) - -(* NOTATION -Notation h := RS'_h. -*) - -(* NOTATION -Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). -*) - -(* NOTATION -Notation just2 := - (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)). -*) - -(* From ftc/Rolle *********************************************************) - -(* NOTATION -Notation cp := (compact_part a b Hab' d Hd). -*) - -(* From ftc/TaylorLemma ***************************************************) - -(* NOTATION -Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a). -*) - -(* NOTATION -Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b). -*) - -(* From ftc/WeakIVT *******************************************************) - -(* NOTATION -Infix "**" := prodT (at level 20). -*) - -(* From metrics/CPseudoMSpaces ********************************************) - -(* NOTATION -Infix "[-d]" := cms_d (at level 68, left associativity). -*) - -(* From model/structures/Nsec *********************************************) - -(* NOTATION -Infix "{#N}" := ap_nat (no associativity, at level 90). -*) - -(* From model/structures/Qsec *********************************************) - -(* NOTATION -Infix "{=Q}" := Qeq (no associativity, at level 90). -*) - -(* NOTATION -Infix "{#Q}" := Qap (no associativity, at level 90). -*) - -(* NOTATION -Infix "{X)->(A->X)/\(B->X). @@ -132,7 +144,7 @@ coercion. *) (* begin hide *) -coercion "cic:/matita/CoRN-Decl/algebra/Basics/Z_of_nat.con" 0 (* compounds *). +coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *). (* end hide *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma index e13a056fb..c603a3517 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbGroups". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/CGroups.ma". @@ -33,7 +33,7 @@ inline "cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con". inline "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CAbGroups/cag_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CAbGroups/cag_crr.con 0 (* compounds *). (* UNEXPORTED Section AbGroup_Axioms. diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma index 9e5eda233..de11ce21a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbMonoids". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/CMonoids.ma". @@ -33,7 +33,7 @@ inline "cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con". inline "cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CAbMonoids/cam_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CAbMonoids/cam_crr.con 0 (* compounds *). (* UNEXPORTED Section AbMonoid_Axioms. diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma index 430accaf6..9b216e081 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CFields". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *) @@ -125,7 +125,7 @@ inline "cic:/CoRN/algebra/CFields/is_CField.con". inline "cic:/CoRN/algebra/CFields/CField.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CFields/cf_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CFields/cf_crr.con 0 (* compounds *). (* End_SpecReals *) @@ -149,6 +149,10 @@ inline "cic:/CoRN/algebra/CFields/cf_div.con". Implicit Arguments cf_div [F]. *) +(* NOTATION +Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80). +*) + (*#* %\begin{convention}\label{convention:div-form}% - Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy]. @@ -559,10 +563,18 @@ End CField_Ops. Implicit Arguments Frecip [X]. *) +(* NOTATION +Notation "{1/} x" := (Frecip x) (at level 2, right associativity). +*) + (* UNEXPORTED Implicit Arguments Fdiv [X]. *) +(* NOTATION +Infix "{/}" := Fdiv (at level 41, no associativity). +*) + (* UNEXPORTED Hint Resolve included_FRecip included_FDiv : included. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma index 42287b0e2..6e644810b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *) @@ -47,7 +47,7 @@ inline "cic:/CoRN/algebra/CGroups/is_CGroup.con". inline "cic:/CoRN/algebra/CGroups/CGroup.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con 0 (* compounds *). (* End_SpecReals *) @@ -57,6 +57,10 @@ coercion "cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con" 0 (* compounds *). Implicit Arguments cg_inv [c]. *) +(* NOTATION +Notation "[--] x" := (cg_inv x) (at level 2, right associativity). +*) + inline "cic:/CoRN/algebra/CGroups/cg_minus.con". (*#* @@ -70,6 +74,10 @@ and [ [-] ] with [minus]. Implicit Arguments cg_minus [G]. *) +(* NOTATION +Infix "[-]" := cg_minus (at level 50, left associativity). +*) + (* End_SpecReals *) (*#* @@ -377,10 +385,18 @@ End CGroup_Ops. Implicit Arguments Finv [G]. *) +(* NOTATION +Notation "{--} x" := (Finv x) (at level 2, right associativity). +*) + (* UNEXPORTED Implicit Arguments Fminus [G]. *) +(* NOTATION +Infix "{-}" := Fminus (at level 50, left associativity). +*) + (* UNEXPORTED Hint Resolve included_FInv included_FMinus : included. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma index 172075946..f0ec034f3 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CLogic". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *) @@ -125,6 +125,10 @@ inline "cic:/CoRN/algebra/CLogic/COr.ind". Some lemmas to make it possible to use [Step] when reasoning with biimplications.*) +(* NOTATION +Infix "IFF" := Iff (at level 60, right associativity). +*) + inline "cic:/CoRN/algebra/CLogic/Iff_left.con". inline "cic:/CoRN/algebra/CLogic/Iff_right.con". @@ -155,6 +159,14 @@ End Basics. (* begin hide *) +(* NOTATION +Infix "or" := COr (at level 85, right associativity). +*) + +(* NOTATION +Infix "and" := CAnd (at level 80, right associativity). +*) + (* end hide *) inline "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con". @@ -163,6 +175,17 @@ inline "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con". (* begin hide *) +(* NOTATION +Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp) + (at level 0, x at level 99) : type_scope. +*) + +(* NOTATION +Notation "{ x : A | P | Q }" := + (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) : + type_scope. +*) + (* end hide *) (* @@ -590,3 +613,11 @@ inline "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con". inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con". +(* NOTATION +Notation ProjT1 := (proj1_sigT _ _). +*) + +(* NOTATION +Notation ProjT2 := (proj2_sigT _ _). +*) + diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma index 553a53083..825673c2b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CMonoids". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CMonoids.v,v 1.3 2004/04/07 15:07:57 lcf Exp $ *) @@ -51,7 +51,7 @@ inline "cic:/CoRN/algebra/CMonoids/is_CMonoid.ind". inline "cic:/CoRN/algebra/CMonoids/CMonoid.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CMonoids/cm_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CMonoids/cm_crr.con 0 (* compounds *). (*#* %\begin{nameconvention}% @@ -70,6 +70,10 @@ In lemmas we will continue to write [x [#] Zero], rather than e.g. for the setoid of non-zeros. *) +(* NOTATION +Notation Zero := (cm_unit _). +*) + inline "cic:/CoRN/algebra/CMonoids/nonZeroP.con". (* End_SpecReals *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma index 3c5fd1480..44d4f7d7a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdAbs". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/COrdFields2.ma". @@ -63,6 +63,10 @@ Declare Right Step AbsSmall_wdr_unfolded. (* begin hide *) +(* NOTATION +Notation ZeroR := (Zero:R). +*) + (* end hide *) inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con". @@ -117,6 +121,10 @@ Declare Right Step AbsSmall_wdr_unfolded. inline "cic:/CoRN/algebra/COrdAbs/absBig.con". +(* NOTATION +Notation AbsBig := (absBig _). +*) + inline "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con". (* UNEXPORTED diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma index f630d6a1e..70c46d57a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdCauchy". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/COrdAbs.ma". @@ -70,7 +70,7 @@ with the coercions inline "cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind". -coercion "cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con 0 (* compounds *). inline "cic:/CoRN/algebra/COrdCauchy/SeqLimit.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma index dfd8583ea..dd9b0c82d 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: COrdFields.v,v 1.6 2004/04/23 10:00:52 lcf Exp $ *) @@ -83,7 +83,7 @@ inline "cic:/CoRN/algebra/COrdFields/is_COrdField.ind". inline "cic:/CoRN/algebra/COrdFields/COrdField.ind". -coercion "cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con 0 (* compounds *). (*#* %\begin{nameconvention}% @@ -96,12 +96,20 @@ is written as [pos]. Implicit Arguments cof_less [c]. *) +(* NOTATION +Infix "[<]" := cof_less (at level 70, no associativity). +*) + inline "cic:/CoRN/algebra/COrdFields/greater.con". (* UNEXPORTED Implicit Arguments greater [F]. *) +(* NOTATION +Infix "[>]" := greater (at level 70, no associativity). +*) + (* End_SpecReals *) (*#* @@ -121,6 +129,10 @@ In the names of lemmas, [ [<=] ] is written as [leEq] and Implicit Arguments leEq [F]. *) +(* NOTATION +Infix "[<=]" := leEq (at level 70, no associativity). +*) + (* UNEXPORTED Section COrdField_axioms. *) @@ -406,6 +418,54 @@ Declare Left Step leEq_wdl. Declare Right Step leEq_wdr. *) +(* NOTATION +Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20). +*) + (* UNEXPORTED Section consequences_of_infinity. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma index 5b8d8cdbb..59b5d94ee 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields2". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/COrdFields.ma". @@ -252,6 +252,14 @@ inline "cic:/CoRN/algebra/COrdFields2/R.var". (* begin hide *) +(* NOTATION +Notation ZeroR := (Zero:R). +*) + +(* NOTATION +Notation OneR := (One:R). +*) + (* end hide *) inline "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma index 2da1436b8..fd7835ba5 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_ApZero". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPoly_ApZero.v,v 1.3 2004/04/23 10:00:53 lcf Exp $ *) @@ -59,6 +59,10 @@ inline "cic:/CoRN/algebra/CPoly_ApZero/degree_f.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) include "tactics/Transparent_algebra.ma". @@ -146,6 +150,10 @@ inline "cic:/CoRN/algebra/CPoly_ApZero/H.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) inline "cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con". @@ -172,6 +180,10 @@ inline "cic:/CoRN/algebra/CPoly_ApZero/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) inline "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma index 475c1e5b5..038c3f3c4 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_Degree". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPoly_Degree.v,v 1.5 2004/04/23 10:00:53 lcf Exp $ *) @@ -40,6 +40,10 @@ inline "cic:/CoRN/algebra/CPoly_Degree/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) (*#* @@ -108,6 +112,10 @@ inline "cic:/CoRN/algebra/CPoly_Degree/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con". @@ -218,6 +226,10 @@ inline "cic:/CoRN/algebra/CPoly_Degree/F.var". (* begin hide *) +(* NOTATION +Notation FX := (cpoly_cring F). +*) + (* end hide *) inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma index e2b643b28..ae0db8884 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_NthCoeff". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPoly_NthCoeff.v,v 1.6 2004/04/23 10:00:53 lcf Exp $ *) @@ -39,6 +39,10 @@ inline "cic:/CoRN/algebra/CPoly_NthCoeff/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) (*#* @@ -115,6 +119,10 @@ inline "cic:/CoRN/algebra/CPoly_NthCoeff/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_zero.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma index 908bdbece..ce31278d6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPolynomials". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPolynomials.v,v 1.9 2004/04/23 10:00:53 lcf Exp $ *) @@ -335,6 +335,10 @@ inline "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con". Implicit Arguments cpoly_linear_fun' [CR]. *) +(* NOTATION +Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity). +*) + (*#* ** Apartness, equality, and induction %\label{section:poly-equality}% *) @@ -352,6 +356,10 @@ elements of the ring. inline "cic:/CoRN/algebra/CPolynomials/CR.var". +(* NOTATION +Notation RX := (cpoly_cring CR). +*) + (* UNEXPORTED Section helpful_section. *) @@ -451,6 +459,10 @@ In the names of lemmas, we write [apply]. Implicit Arguments cpoly_apply_fun [CR]. *) +(* NOTATION +Infix "!" := cpoly_apply_fun (at level 1, no associativity). +*) + (*#* ** Basic properties of polynomials %\begin{convention}% @@ -464,6 +476,10 @@ Section Poly_properties. inline "cic:/CoRN/algebra/CPolynomials/R.var". +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (*#* *** Constant and identity *) @@ -578,6 +594,22 @@ Section Poly_Prop_Induction. inline "cic:/CoRN/algebra/CPolynomials/CR.var". +(* NOTATION +Notation Cpoly := (cpoly CR). +*) + +(* NOTATION +Notation Cpoly_zero := (cpoly_zero CR). +*) + +(* NOTATION +Notation Cpoly_linear := (cpoly_linear CR). +*) + +(* NOTATION +Notation Cpoly_cring := (cpoly_cring CR). +*) + inline "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con". (* UNEXPORTED diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma index 9210cad60..4a79f1220 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CRings". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *) @@ -83,7 +83,7 @@ inline "cic:/CoRN/algebra/CRings/is_CRing.ind". inline "cic:/CoRN/algebra/CRings/CRing.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con 0 (* compounds *). inline "cic:/CoRN/algebra/CRings/cr_plus.con". @@ -91,6 +91,10 @@ inline "cic:/CoRN/algebra/CRings/cr_inv.con". inline "cic:/CoRN/algebra/CRings/cr_minus.con". +(* NOTATION +Notation One := (cr_one _). +*) + (* End_SpecReals *) (* Begin_SpecReals *) @@ -106,6 +110,10 @@ and [[*]] with [mult]. Implicit Arguments cr_mult [c]. *) +(* NOTATION +Infix "[*]" := cr_mult (at level 40, left associativity). +*) + (* UNEXPORTED Section CRing_axioms. *) @@ -356,6 +364,10 @@ End exponentiation. (* End_SpecReals *) +(* NOTATION +Notation "x [^] n" := (nexp_op _ n x) (at level 20). +*) + (* UNEXPORTED Implicit Arguments nexp_op [R]. *) @@ -410,6 +422,50 @@ Implicit Arguments nring [R]. (* End_SpecReals *) +(* NOTATION +Notation Two := (nring 2). +*) + +(* NOTATION +Notation Three := (nring 3). +*) + +(* NOTATION +Notation Four := (nring 4). +*) + +(* NOTATION +Notation Six := (nring 6). +*) + +(* NOTATION +Notation Eight := (nring 8). +*) + +(* NOTATION +Notation Twelve := (nring 12). +*) + +(* NOTATION +Notation Sixteen := (nring 16). +*) + +(* NOTATION +Notation Nine := (nring 9). +*) + +(* NOTATION +Notation Eighteen := (nring 18). +*) + +(* NOTATION +Notation TwentyFour := (nring 24). +*) + +(* NOTATION +Notation FortyEight := (nring 48). +*) + inline "cic:/CoRN/algebra/CRings/one_plus_one.con". inline "cic:/CoRN/algebra/CRings/x_plus_x.con". @@ -902,14 +958,26 @@ inline "cic:/CoRN/algebra/CRings/Fscalmult.con". Implicit Arguments Fmult [R]. *) +(* NOTATION +Infix "{*}" := Fmult (at level 40, left associativity). +*) + (* UNEXPORTED Implicit Arguments Fscalmult [R]. *) +(* NOTATION +Infix "{**}" := Fscalmult (at level 40, left associativity). +*) + (* UNEXPORTED Implicit Arguments Fnth [R]. *) +(* NOTATION +Infix "{^}" := Fnth (at level 30, right associativity). +*) + (* UNEXPORTED Section ScalarMultiplication. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma index b63dd3175..85eac7de2 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSemiGroups". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CSemiGroups.v,v 1.8 2004/04/22 14:49:43 lcf Exp $ *) @@ -37,7 +37,7 @@ inline "cic:/CoRN/algebra/CSemiGroups/is_CSemiGroup.con". inline "cic:/CoRN/algebra/CSemiGroups/CSemiGroup.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con 0 (* compounds *). (*#* %\begin{nameconvention}% @@ -49,6 +49,10 @@ In the %{\em %names%}% of lemmas, we will denote [[+]] with [plus]. Implicit Arguments csg_op [c]. *) +(* NOTATION +Infix "[+]" := csg_op (at level 50, left associativity). +*) + (* End_SpecReals *) (*#* **Semigroup axioms @@ -156,6 +160,10 @@ End Part_Function_Plus. Implicit Arguments Fplus [G]. *) +(* NOTATION +Infix "{+}" := Fplus (at level 50, left associativity). +*) + (* UNEXPORTED Hint Resolve included_FPlus : included. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma index ef647e71f..84c0c6c26 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoidFun". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *) @@ -249,6 +249,10 @@ End Extension. End SubSets_of_G. *) +(* NOTATION +Notation Conj := (conjP _). +*) + (* UNEXPORTED Implicit Arguments disj [S]. *) @@ -272,7 +276,11 @@ We are now ready to define the concept of partial function between arbitrary set inline "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *). + +(* NOTATION +Notation BDom := (bpfdom _ _). +*) (* UNEXPORTED Implicit Arguments bpfpfun [S1 S2]. @@ -288,7 +296,15 @@ inline "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con". inline "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con 0 (* compounds *). + +(* NOTATION +Notation Dom := (pfdom _). +*) + +(* NOTATION +Notation Part := (pfpfun _). +*) (* UNEXPORTED Implicit Arguments pfpfun [S]. @@ -475,10 +491,22 @@ End BinPart_Function_Composition. Implicit Arguments Fconst [S]. *) +(* NOTATION +Notation "[-C-] x" := (Fconst x) (at level 2, right associativity). +*) + +(* NOTATION +Notation FId := (Fid _). +*) + (* UNEXPORTED Implicit Arguments Fcomp [S]. *) +(* NOTATION +Infix "[o]" := Fcomp (at level 65, no associativity). +*) + (* UNEXPORTED Hint Resolve pfwdef bpfwdef: algebra. *) @@ -581,3 +609,11 @@ Implicit Arguments Inv [A B]. Implicit Arguments conj_wd [S P Q]. *) +(* NOTATION +Notation Prj1 := (prj1 _ _ _ _). +*) + +(* NOTATION +Notation Prj2 := (prj2 _ _ _ _). +*) + diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma index 571689093..ad6490a75 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoidInc". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma index bda5ded20..2f1ed75ca 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoids". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *) @@ -131,7 +131,7 @@ inline "cic:/CoRN/algebra/CSetoids/is_CSetoid.ind". inline "cic:/CoRN/algebra/CSetoids/CSetoid.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/cs_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/cs_crr.con 0 (* compounds *). (* UNEXPORTED Implicit Arguments cs_eq [c]. @@ -141,6 +141,14 @@ Implicit Arguments cs_eq [c]. Implicit Arguments cs_ap [c]. *) +(* NOTATION +Infix "[=]" := cs_eq (at level 70, no associativity). +*) + +(* NOTATION +Infix "[#]" := cs_ap (at level 70, no associativity). +*) + (* End_SpecReals *) inline "cic:/CoRN/algebra/CSetoids/cs_neq.con". @@ -149,6 +157,10 @@ inline "cic:/CoRN/algebra/CSetoids/cs_neq.con". Implicit Arguments cs_neq [S]. *) +(* NOTATION +Infix "[~=]" := cs_neq (at level 70, no associativity). +*) + (*#* %\begin{nameconvention}% In the names of lemmas, we refer to [ [=] ] by [eq], [ [~=] ] by @@ -364,7 +376,7 @@ End CSetoidPredicates. inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csp_pred.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csp_pred.con 0 (* compounds *). inline "cic:/CoRN/algebra/CSetoids/csp_wd.con". @@ -388,7 +400,7 @@ End CSetoidPPredicates. inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csp'_pred.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csp'_pred.con 0 (* compounds *). inline "cic:/CoRN/algebra/CSetoids/csp'_wd.con". @@ -434,7 +446,7 @@ The type of relations over a setoid. *) inline "cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csr_rel.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csr_rel.con 0 (* compounds *). (*#* ***[CProp] Relations %\begin{convention}% @@ -478,7 +490,7 @@ The type of relations over a setoid. *) inline "cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/Ccsr_rel.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *). inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con". @@ -564,7 +576,7 @@ End unary_functions. inline "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csf_fun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csf_fun.con 0 (* compounds *). inline "cic:/CoRN/algebra/CSetoids/csf_wd.con". @@ -602,7 +614,7 @@ End binary_functions. inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csbf_fun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/csbf_fun.con 0 (* compounds *). inline "cic:/CoRN/algebra/CSetoids/csbf_wd.con". @@ -677,7 +689,7 @@ inline "cic:/CoRN/algebra/CSetoids/id_un_op.con". (* begin hide *) -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/un_op_fun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/un_op_fun.con 0 (* compounds *). (* end hide *) @@ -713,7 +725,7 @@ inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con". (* begin hide *) -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/bin_op_bin_fun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *). (* end hide *) @@ -791,7 +803,7 @@ inline "cic:/CoRN/algebra/CSetoids/csoo_strext.con". (* begin hide *) -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/outer_op_bin_fun.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *). (* end hide *) @@ -823,7 +835,7 @@ inline "cic:/CoRN/algebra/CSetoids/P.var". inline "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/scs_elem.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CSetoids/scs_elem.con 0 (* compounds *). (*#* Though [scs_elem] is declared as a coercion, it does not satisfy the uniform inheritance condition and will not be inserted. However it will diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma index 133a29096..b0fc1c6a2 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma index 6b2f8969a..76324bcdd 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CVectorSpace". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CVectorSpace.v,v 1.4 2004/04/23 10:00:54 lcf Exp $ *) @@ -44,7 +44,7 @@ Unset Strict Implicit. inline "cic:/CoRN/algebra/CVectorSpace/VSpace.ind". -coercion "cic:/matita/CoRN-Decl/algebra/CVectorSpace/vs_vs.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/CVectorSpace/vs_vs.con 0 (* compounds *). (* begin hide *) @@ -66,6 +66,10 @@ Hint Resolve vs_assoc vs_unit vs_distl vs_distr: algebra. Implicit Arguments vs_op [F v]. *) +(* NOTATION +Infix "[']" := vs_op (at level 30, no associativity). +*) + (*#* %\begin{convention}% Let [F] be a fiels and let [V] be a vector space over [F] diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma index 6505106ad..7070c44d8 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Expon.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Expon.ma index d4b468438..d2e834f66 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/Expon.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Expon.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Expon". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Expon.v,v 1.5 2004/04/23 10:00:54 lcf Exp $ *) @@ -116,6 +116,10 @@ End Zexp_def. Implicit Arguments zexp [R]. *) +(* NOTATION +Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0). +*) + (*#* **Properties of [zexp] %\begin{convention}% Let [R] be an ordered field. %\end{convention}% diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma index b4a8978be..1decb2491 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/ListType.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/ListType". -include "CoRN_notation.ma". +include "CoRN.ma". (* begin hide *) diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/AbsCC.ma b/helm/software/matita/contribs/CoRN-Decl/complex/AbsCC.ma index b6aee2079..e2d902b9b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/complex/AbsCC.ma +++ b/helm/software/matita/contribs/CoRN-Decl/complex/AbsCC.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/AbsCC". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: AbsCC.v,v 1.2 2004/04/23 10:00:54 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma b/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma index c28c05ed1..2782cf035 100644 --- a/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma +++ b/helm/software/matita/contribs/CoRN-Decl/complex/CComplex.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/CComplex". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CComplex.v,v 1.8 2004/04/23 10:00:55 lcf Exp $ *) @@ -194,10 +194,18 @@ End Complex_Numbers. (* begin hide *) +(* NOTATION +Notation CCX := (cpoly_cring CC). +*) + (* end hide *) inline "cic:/CoRN/complex/CComplex/II.con". +(* NOTATION +Infix "[+I*]" := cc_set_CC (at level 48, no associativity). +*) + (*#* ** Properties of [II] *) (* UNEXPORTED diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma b/helm/software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma index 13be938dc..228a19f5a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma +++ b/helm/software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/Complex_Exponential". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Complex_Exponential.v,v 1.4 2004/04/23 10:00:55 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma b/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma index ff7b39956..b8fe0878b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma +++ b/helm/software/matita/contribs/CoRN-Decl/complex/NRootCC.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma b/helm/software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma index b63b890ff..f99d50781 100644 --- a/helm/software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma +++ b/helm/software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/IDA/Ch6". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/CSemiGroups.ma". diff --git a/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma b/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma index 92ee5fe37..88fcfbeb9 100644 --- a/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma +++ b/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/csetfun". -include "CoRN_notation.ma". +include "CoRN.ma". include "algebra/CSetoids.ma". diff --git a/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma b/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma index 799d0636d..e41d74f18 100644 --- a/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma +++ b/helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma @@ -16,13 +16,13 @@ set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun". -include "CoRN_notation.ma". +include "CoRN.ma". inline "cic:/CoRN/devel/loeb/per/lst2fun/F'.con". inline "cic:/CoRN/devel/loeb/per/lst2fun/F.ind". -coercion "cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun/F_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun/F_crr.con 0 (* compounds *). inline "cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con". @@ -30,7 +30,7 @@ inline "cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con". Implicit Arguments to_nat [n]. *) -coercion "cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun/to_nat.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/devel/loeb/per/lst2fun/to_nat.con 0 (* compounds *). include "algebra/CSetoids.ma". diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/CC_Props.ma b/helm/software/matita/contribs/CoRN-Decl/fta/CC_Props.ma index d61fb9856..1203f8688 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/CC_Props.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/CC_Props.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/CC_Props". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CC_Props.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *) @@ -41,7 +41,7 @@ inline "cic:/CoRN/fta/CC_Props/CC_Cauchy_prop.con". inline "cic:/CoRN/fta/CC_Props/CC_CauchySeq.ind". -coercion "cic:/matita/CoRN-Decl/fta/CC_Props/CC_seq.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/fta/CC_Props/CC_seq.con 0 (* compounds *). inline "cic:/CoRN/fta/CC_Props/re_is_Cauchy.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma b/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma index aa60f0e0f..c331e5e37 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Contin1". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPoly_Contin1.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma b/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma index 00a91c8f8..32961ffe2 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Rev". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPoly_Rev.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma b/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma index eadff2abc..e0875e59f 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Shift". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPoly_Shift.v,v 1.4 2004/04/23 10:00:56 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/FTA.ma b/helm/software/matita/contribs/CoRN-Decl/fta/FTA.ma index 8f8bd91b5..ba69c7ec6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/FTA.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/FTA.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/FTA". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: FTA.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/FTAreg.ma b/helm/software/matita/contribs/CoRN-Decl/fta/FTAreg.ma index 3db7923fd..0835edf40 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/FTAreg.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/FTAreg.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/FTAreg". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: FTAreg.v,v 1.4 2004/04/23 10:00:57 lcf Exp $ *) @@ -73,11 +73,11 @@ inline "cic:/CoRN/fta/FTAreg/p0ltc0.var". inline "cic:/CoRN/fta/FTAreg/Knes_tup.ind". -coercion "cic:/matita/CoRN-Decl/fta/FTAreg/z_el.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/fta/FTAreg/z_el.con 0 (* compounds *). inline "cic:/CoRN/fta/FTAreg/Knes_tupp.ind". -coercion "cic:/matita/CoRN-Decl/fta/FTAreg/Kntup.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/fta/FTAreg/Kntup.con 0 (* compounds *). inline "cic:/CoRN/fta/FTAreg/Knes_fun.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma b/helm/software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma index 874544bf2..caf87bea1 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/KeyLemma". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma b/helm/software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma index 8b659c74d..fbbeb1c49 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/KneserLemma". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: KneserLemma.v,v 1.7 2004/04/23 10:00:57 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/fta/MainLemma.ma b/helm/software/matita/contribs/CoRN-Decl/fta/MainLemma.ma index 6ce6411da..350e62138 100644 --- a/helm/software/matita/contribs/CoRN-Decl/fta/MainLemma.ma +++ b/helm/software/matita/contribs/CoRN-Decl/fta/MainLemma.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/fta/MainLemma". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: MainLemma.v,v 1.3 2004/04/23 10:00:57 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma index ce11a7538..bf7461582 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/COrdLemmas". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: COrdLemmas.v,v 1.2 2004/04/23 10:00:57 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma index fd17db69e..6e43129c3 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/CalculusTheorems". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CalculusTheorems.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Composition.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Composition.ma index 26aef79e1..124656d5b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Composition.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Composition.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Composition". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma index 1f205d3e8..113b47653 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Continuity". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Derivative.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Derivative.ma index b02b64a2b..4551cb741 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Derivative.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Derivative.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Derivative". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Derivative.v,v 1.7 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma index 9d4b236da..25a674c26 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/DerivativeOps". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: DerivativeOps.v,v 1.3 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma index 6e49315ea..ded63db55 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Differentiability". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma index 9414971c8..5d764a882 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FTC". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *) @@ -75,6 +75,10 @@ End Indefinite_Integral. Implicit Arguments Fprim [I F]. *) +(* NOTATION +Notation "[-S-] F" := (Fprim F) (at level 20). +*) + (* UNEXPORTED Section FTC. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma index 36e2f5016..768b71285 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSequence". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma index 76cfcdcf6..869a6a3f9 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSeries". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma index d5d45d4a8..aeed9200c 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma index 920dcdbfc..a6bace36d 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Integral". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *) @@ -160,6 +160,10 @@ inline "cic:/CoRN/ftc/Integral/I.con". (* end hide *) +(* NOTATION +Notation Integral := (integral _ _ Hab). +*) + (* UNEXPORTED Section Well_Definedness. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma index f2af4cc82..bf128f9a0 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/IntervalFunct". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma index 8fca8e19f..20eaa0dcd 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunSeries". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma index f8d53d6d3..71333c0bd 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunctions". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma index f48c65d40..50a087bf7 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntegrals". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma index c3abe0aa6..40719fd59 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntervals". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *) @@ -111,7 +111,7 @@ inline "cic:/CoRN/ftc/MoreIntervals/iprop.con". (* begin hide *) -coercion "cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con 0 (* compounds *). (* end hide *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma index bd2735e2f..0900e8703 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/NthDerivative". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma index a948192b3..c3b8f1c56 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartFunEquality". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma index 3013ac376..47e164663 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartInterval". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Partitions.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Partitions.ma index 46d1a4528..58a7651fc 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Partitions.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Partitions.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Partitions". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *) @@ -52,7 +52,7 @@ coercion); inline "cic:/CoRN/ftc/Partitions/Partition.ind". -coercion "cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con 0 (* compounds *). (*#* Two immediate consequences of this are that [ai [<=] aj] whenever [i < j] and that [ai] is in [[a,b]] for all [i]. diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma index 99ca5a648..9503e78c1 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefLemma". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *) @@ -186,8 +186,24 @@ inline "cic:/CoRN/ftc/RefLemma/RL_h.con". inline "cic:/CoRN/ftc/RefLemma/RL_g.con". +(* NOTATION +Notation g := RL_g. +*) + +(* NOTATION +Notation h := RL_h. +*) + inline "cic:/CoRN/ftc/RefLemma/ref_calc1.con". +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)). +*) + +(* NOTATION +Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)). +*) + inline "cic:/CoRN/ftc/RefLemma/ref_calc2.con". inline "cic:/CoRN/ftc/RefLemma/ref_calc3.con". @@ -428,6 +444,10 @@ Section Fourth_Refinement_Lemma. inline "cic:/CoRN/ftc/RefLemma/Fa.con". +(* NOTATION +Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)). +*) + inline "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con". (* end hide *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma index de7f771ec..ab403b372 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSepRef". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: RefSepRef.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma index b082b83c8..440ec7a98 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparated". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *) @@ -160,6 +160,15 @@ inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con". inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con". +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). +*) + +(* NOTATION +Notation just2 := + (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)). +*) + inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con". inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma index 8b2081547..4a30dc549 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparating". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: RefSeparating.v,v 1.7 2004/04/23 10:01:01 lcf Exp $ *) @@ -98,6 +98,10 @@ inline "cic:/CoRN/ftc/RefSeparating/RS'_m1.con". inline "cic:/CoRN/ftc/RefSeparating/RS'_m.con". +(* NOTATION +Notation m := RS'_m. +*) + inline "cic:/CoRN/ftc/RefSeparating/sep__part_length.con". inline "cic:/CoRN/ftc/RefSeparating/RS'_m_m1.con". @@ -148,6 +152,19 @@ inline "cic:/CoRN/ftc/RefSeparating/RS'_Hsep.con". inline "cic:/CoRN/ftc/RefSeparating/RS'_h.con". +(* NOTATION +Notation h := RS'_h. +*) + +(* NOTATION +Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). +*) + +(* NOTATION +Notation just2 := + (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)). +*) + inline "cic:/CoRN/ftc/RefSeparating/sep__part_suRS'_m1.con". inline "cic:/CoRN/ftc/RefSeparating/sep__part_Sum2.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma index bbb05b7fa..7eda2c5ae 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Rolle". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Rolle.v,v 1.6 2004/04/23 10:01:01 lcf Exp $ *) @@ -112,6 +112,10 @@ inline "cic:/CoRN/ftc/Rolle/incF'.con". inline "cic:/CoRN/ftc/Rolle/fcp'.con". +(* NOTATION +Notation cp := (compact_part a b Hab' d Hd). +*) + inline "cic:/CoRN/ftc/Rolle/Rolle_lemma4.con". inline "cic:/CoRN/ftc/Rolle/Rolle_lemma5.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma index f60b9b213..fe8820e0a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/StrongIVT". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: StrongIVT.v,v 1.5 2004/04/23 10:01:01 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma index 89301438d..9a9437ade 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Taylor.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Taylor". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Taylor.v,v 1.10 2004/04/23 10:01:01 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma index be23aede5..7f704092e 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/TaylorLemma". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *) @@ -98,6 +98,14 @@ inline "cic:/CoRN/ftc/TaylorLemma/TL_compact_a.con". inline "cic:/CoRN/ftc/TaylorLemma/TL_compact_b.con". +(* NOTATION +Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a). +*) + +(* NOTATION +Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b). +*) + (* end hide *) (* begin show *) diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma index 3e49ac89d..8001b5376 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/WeakIVT". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *) @@ -24,6 +24,10 @@ include "CoRN_notation.ma". (* begin hide *) +(* NOTATION +Infix "**" := prodT (at level 20). +*) + (* end hide *) include "ftc/Continuity.ma". diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma index 7f4dedf08..c50761c19 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/CMetricSpaces". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *) @@ -33,7 +33,7 @@ Section Definition_MS. inline "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind". -coercion "cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *). (* UNEXPORTED End Definition_MS. diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma index 5875e22f4..aef56d5a9 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPMSTheory". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma index 310b633ef..a22750116 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CPseudoMSpaces.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *) @@ -87,7 +87,7 @@ inline "cic:/CoRN/metrics/CPseudoMSpaces/is_CPsMetricSpace.ind". inline "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace.ind". -coercion "cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces/cms_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *). (* UNEXPORTED End Definition_PsMS0. @@ -97,6 +97,10 @@ End Definition_PsMS0. Implicit Arguments cms_d [c]. *) +(* NOTATION +Infix "[-d]" := cms_d (at level 68, left associativity). +*) + (* UNEXPORTED Section PsMS_axioms. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma index e4065b80a..0f93560af 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/ContFunctions". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: ContFunctions.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/Equiv.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/Equiv.ma index b8caaf66e..037029733 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/Equiv.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/Equiv.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/Equiv". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Equiv.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma index e6bbef939..1bd2da730 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/IR_CPMSpace". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: IR_CPMSpace.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma index d73d2ff07..f30b3c65d 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/metrics/Prod_Sub". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Prod_Sub.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma index 13d235e17..4e6f57e8c 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/QSposabgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: QSposabgroup.v,v 1.5 2004/04/08 08:20:31 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma index 7e410fe32..57c6da7d6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Qabgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qabgroup.v,v 1.5 2004/04/08 08:20:31 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma index 34839f78d..4c5f2b2d9 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Qposabgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qposabgroup.v,v 1.6 2004/04/08 08:20:31 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma index 6c13b0f29..0cfc20cca 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/Zabgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Zabgroup.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma b/helm/software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma index 3ea733862..8024b79f3 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/fields/Qfield". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qfield.v,v 1.8 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma index 90cf73548..99993bd80 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/groups/QSposgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: QSposgroup.v,v 1.6 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma index 8919083f1..e508583d6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/groups/Qgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qgroup.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma index 469bd19ea..02e0b6c33 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/groups/Qposgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qposgroup.v,v 1.6 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma index 455b23e85..3f5430193 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/groups/Zgroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Zgroup.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma index 010840492..4eac5c0c6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Nmonoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Nmonoid.v,v 1.5 2004/04/08 08:20:32 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma index e52e750f9..1d23f7d4a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Nposmonoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Nposmonoid.v,v 1.6 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma index 0ee690572..0ec63cd7b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/QSposmonoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: QSposmonoid.v,v 1.5 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma index b4434c47b..e19460778 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Qmonoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qmonoid.v,v 1.7 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma index 1ca152f29..e8f9f96ee 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Qposmonoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qposmonoid.v,v 1.7 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma index 6839514fe..d6b0ddea4 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/monoids/Zmonoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Zmonoid.v,v 1.6 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma b/helm/software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma index 16a47b18a..260cc8d68 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/non_examples/N_no_group". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: N_no_group.v,v 1.5 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma b/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma index 468322636..7f86667be 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/non_examples/Npos_no_group". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Npos_no_group.v,v 1.6 2004/04/08 08:20:33 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma index 2846b45af..7dbff7050 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/non_examples/Npos_no_monoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Npos_no_monoid.v,v 1.5 2004/04/08 08:20:34 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma b/helm/software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma index c414588ef..0729946f3 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/ordfields/Qordfield". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qordfield.v,v 1.9 2004/04/23 10:01:03 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma b/helm/software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma index 73bc2f419..a355fe3ed 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/reals/Cauchy_IR". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Cauchy_IR.v,v 1.2 2004/04/06 15:46:03 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/rings/Qring.ma b/helm/software/matita/contribs/CoRN-Decl/model/rings/Qring.ma index 899e2392d..5a1723d1c 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/rings/Qring.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/rings/Qring.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/rings/Qring". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qring.v,v 1.8 2004/04/23 10:01:03 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/rings/Zring.ma b/helm/software/matita/contribs/CoRN-Decl/model/rings/Zring.ma index 18210726e..3927f4332 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/rings/Zring.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/rings/Zring.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/rings/Zring". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Zring.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma index 1f336d815..466677d04 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Npossemigroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Npossemigroup.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma index 88392ac8a..393e00359 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Nsemigroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Nsemigroup.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma index 696fa43e4..54eb20c11 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/QSpossemigroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: QSpossemigroup.v,v 1.5 2004/04/08 08:20:35 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma index 8d54a984b..f4336222a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Qpossemigroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qpossemigroup.v,v 1.6 2004/04/08 08:20:35 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma index 12225b61d..09fbc4aca 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Qsemigroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qsemigroup.v,v 1.6 2004/04/08 08:20:35 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma index d79f3598f..4ec6a0ac6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/semigroups/Zsemigroup". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Zsemigroup.v,v 1.6 2004/04/08 08:20:35 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma index e450d4950..23363a170 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Npossetoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Npossetoid.v,v 1.3 2004/04/06 15:46:04 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma index 975d61eec..b3bf1fc3d 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Nsetoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Nsetoid.v,v 1.4 2004/04/06 15:46:04 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma index 51add6524..9557dc175 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Qpossetoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qpossetoid.v,v 1.4 2004/04/06 15:46:05 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma index 4167c5617..71cdafa4a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Qsetoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qsetoid.v,v 1.6 2004/04/06 15:46:05 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma index 5d38b80bd..84541c4db 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/setoids/Zsetoid". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Zsetoid.v,v 1.5 2004/04/07 15:08:08 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma b/helm/software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma index e96cb00d7..7a47323f6 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Npossec". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Npossec.v,v 1.3 2004/04/06 15:46:05 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma b/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma index 78e509a0b..084be106c 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Nsec". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Nsec.v,v 1.6 2004/04/06 15:46:05 lcf Exp $ *) @@ -39,6 +39,10 @@ inline "cic:/CoRN/model/structures/Nsec/S_O.con". inline "cic:/CoRN/model/structures/Nsec/ap_nat.con". +(* NOTATION +Infix "{#N}" := ap_nat (no associativity, at level 90). +*) + inline "cic:/CoRN/model/structures/Nsec/ap_nat_irreflexive0.con". inline "cic:/CoRN/model/structures/Nsec/ap_nat_symmetric0.con". diff --git a/helm/software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma b/helm/software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma index d8c5e38f2..38f43ac38 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Qpossec". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qpossec.v,v 1.5 2004/04/06 15:46:05 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma b/helm/software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma index 8f677c178..595c037a0 100644 --- a/helm/software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma +++ b/helm/software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Qsec". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Qsec.v,v 1.7 2004/04/08 08:20:35 lcf Exp $ *) @@ -74,6 +74,30 @@ inline "cic:/CoRN/model/structures/Qsec/Qinv.con". End Q. *) +(* NOTATION +Infix "{=Q}" := Qeq (no associativity, at level 90). +*) + +(* NOTATION +Infix "{#Q}" := Qap (no associativity, at level 90). +*) + +(* NOTATION +Infix "{y=ey*log(x)#, whenever inline "cic:/CoRN/transc/RealPowers/power.con". +(* NOTATION +Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20). +*) + (*#* This definition yields a well defined, strongly extensional function which extends the algebraic exponentiation to an integer power and @@ -153,6 +157,10 @@ inline "cic:/CoRN/transc/RealPowers/Continuous_power.con". End Power_Function. *) +(* NOTATION +Notation "F {!} G" := (FPower F G) (at level 20). +*) + (* UNEXPORTED Section More_on_Power_Function. *) diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma b/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma index f302c538d..4a226195f 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/SinCos.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/SinCos". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma b/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma index a6dd75ab7..74966e1d9 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/TaylorSeries". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/TrigMon.ma b/helm/software/matita/contribs/CoRN-Decl/transc/TrigMon.ma index e3760aa43..7307c4f5a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/TrigMon.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/TrigMon.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/TrigMon". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: TrigMon.v,v 1.9 2004/04/23 10:01:08 lcf Exp $ *) diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma b/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma index a3c098524..de100d310 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/Trigonometric". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)