<?xml version="1.0" encoding="utf-8"?>
<helm_registry>
<section name="package">
- <key name="name">CoRN</key>
+ <key name="input_name">CoRN</key>
+ <key name="output_name">CoRN-Decl</key>
<key name="input_base_uri">cic:/CoRN</key>
<key name="output_base_uri">cic:/matita/CoRN-Decl</key>
<key name="input_path">/projects/helm/exportation/CoRN</key>
<key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
<key name="script_type">.v</key>
+ <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt</key>
</section>
</helm_registry>
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
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
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
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
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
| 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
* http://cs.unibo.it/helm/.
*)
+type local = bool
+
type inline_kind = Con | Ind | Var
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
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 <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
%token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
;
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 }
| 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
| 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:
(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
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
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;
val int: string -> int
val float: string -> float
val bool: string -> bool
+val pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
(** {3 Typed getters} *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "{<Q}" := Qlt (no associativity, at level 90).
+*)
+
+(* NOTATION
+Infix "{+Q}" := Qplus (no associativity, at level 85).
+*)
+
+(* NOTATION
+Infix "{*Q}" := Qmult (no associativity, at level 80).
+*)
+
+(* NOTATION
+Notation "{-Q}" := Qopp (at level 1, left associativity).
+*)
+
+coercion cic:/CoRN/model/structures/Qsec/inject_Z.con 0 (* compounds *).
+
+(* From model/structures/Zsec *********************************************)
+
+(* NOTATION
+Infix "{#Z}" := ap_Z (no associativity, at level 90).
+*)
+
+coercion cic:/CoRN/model/structures/Zsec/Zpos.con 0 (* compounds *).
+
+(* From reals/Bridges_LUB *************************************************)
+
+(* NOTATION
+Notation "( p , q )" := (pairT p q).
+*)
+
+(* From reals/CMetricFields ***********************************************)
+
+coercion cic:/CoRN/reals/CMetricFields/cmf_crr.con 0 (* compounds *).
+
+(* NOTATION
+Notation MAbs := (cmf_abs _).
+*)
+
+coercion cic:/CoRN/reals/CMetricFields/MCS_seq.con 0 (* compounds *).
+
+(* From reals/CReals ******************************************************)
+
+coercion cic:/CoRN/reals/CReals/crl_crr.con 0 (* compounds *).
+
+(* From reals/CauchySeq ***************************************************)
+
+(* NOTATION
+Notation PartIR := (PartFunct IR).
+*)
+
+(* NOTATION
+Notation ProjIR1 := (prj1 IR _ _ _).
+*)
+
+(* NOTATION
+Notation ProjIR2 := (prj2 IR _ _ _).
+*)
+
+(* NOTATION
+Notation ZeroR := (Zero:IR).
+*)
+
+(* NOTATION
+Notation OneR := (One:IR).
+*)
+
+(* From reals/Cauchy_CReals ***********************************************)
+
+(* NOTATION
+Notation "'R_COrdField''" := (R_COrdField F).
+*)
+
+(* From reals/Intervals ***************************************************)
+
+(* NOTATION
+Notation Compact := (compact _ _).
+*)
+
+(* NOTATION
+Notation FRestr := (Frestr (compact_wd _ _ _)).
+*)
+
+(* From reals/Q_dense *****************************************************)
+
+coercion cic:/CoRN/reals/Q_dense/pair_crr.con 0 (* compounds *).
+
+(* NOTATION
+Notation "( A , B )" := (pairT A B).
+*)
+
+(* From reals/Q_in_CReals *************************************************)
+
+coercion cic:/CoRN/reals/Q_in_CReals/nat_of_P.con 0 (* compounds *).
+
+(* From reals/R_morphism **************************************************)
+
+coercion cic:/CoRN/reals/R_morphism/map.con 0 (* compounds *).
+
+(* From tactics/FieldReflection *******************************************)
+
+(* NOTATION
+Notation II := (interpF F val unop binop pfun).
+*)
+
+(* From tactics/GroupReflection *******************************************)
+
+(* NOTATION
+Notation II := (interpG G val unop binop pfun).
+*)
+
+(* From tactics/RingReflection ********************************************)
+
+(* NOTATION
+Notation II := (interpR R val unop binop pfun).
+*)
+
+(* From transc/RealPowers *************************************************)
+
+(* NOTATION
+Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
+*)
+
+(* NOTATION
+Notation "F {!} G" := (FPower F G) (at level 20).
+*)
+
+(* From devel/loeb/per/lst2fun ********************************************)
+
+coercion cic:/CoRN/devel/loeb/per/lst2fun/F_crr.con 0 (* compounds *).
+
+coercion cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con 0 (* compounds *).
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_notation".
-
-(* From algebra/Basics ****************************************************)
-
-(* NOTATION
-Notation Pair := (pair (B:=_)).
-*)
-
-(* NOTATION
-Notation Proj1 := (proj1 (B:=_)).
-*)
-
-(* NOTATION
-Notation Proj2 := (proj2 (B:=_)).
-*)
-
-(* From algebra/CFields ***************************************************)
-
-(* 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 ***************************************************)
-
-(* 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 **************************************************)
-
-(* 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 "{<Q}" := Qlt (no associativity, at level 90).
-*)
-
-(* NOTATION
-Infix "{+Q}" := Qplus (no associativity, at level 85).
-*)
-
-(* NOTATION
-Infix "{*Q}" := Qmult (no associativity, at level 80).
-*)
-
-(* NOTATION
-Notation "{-Q}" := Qopp (at level 1, left associativity).
-*)
-
-(* From model/structures/Zsec *********************************************)
-
-(* NOTATION
-Infix "{#Z}" := ap_Z (no associativity, at level 90).
-*)
-
-(* From reals/Bridges_LUB *************************************************)
-
-(* NOTATION
-Notation "( p , q )" := (pairT p q).
-*)
-
-(* From reals/CMetricFields ***********************************************)
-
-(* NOTATION
-Notation MAbs := (cmf_abs _).
-*)
-
-(* From reals/CauchySeq ***************************************************)
-
-(* NOTATION
-Notation PartIR := (PartFunct IR).
-*)
-
-(* NOTATION
-Notation ProjIR1 := (prj1 IR _ _ _).
-*)
-
-(* NOTATION
-Notation ProjIR2 := (prj2 IR _ _ _).
-*)
-
-(* NOTATION
-Notation ZeroR := (Zero:IR).
-*)
-
-(* NOTATION
-Notation OneR := (One:IR).
-*)
-
-(* From reals/Cauchy_CReals ***********************************************)
-
-(* NOTATION
-Notation "'R_COrdField''" := (R_COrdField F).
-*)
-
-(* From reals/Intervals ***************************************************)
-
-(* NOTATION
-Notation Compact := (compact _ _).
-*)
-
-(* NOTATION
-Notation FRestr := (Frestr (compact_wd _ _ _)).
-*)
-
-(* From reals/Q_dense *****************************************************)
-
-(* NOTATION
-Notation "( A , B )" := (pairT A B).
-*)
-
-(* From tactics/FieldReflection *******************************************)
-
-(* NOTATION
-Notation II := (interpF F val unop binop pfun).
-*)
-
-(* From tactics/GroupReflection *******************************************)
-
-(* NOTATION
-Notation II := (interpG G val unop binop pfun).
-*)
-
-(* From tactics/RingReflection ********************************************)
-
-(* NOTATION
-Notation II := (interpR R val unop binop pfun).
-*)
-
-(* From transc/RealPowers *************************************************)
-
-(* NOTATION
-Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
-*)
-
-(* NOTATION
-Notation "F {!} G" := (FPower F G) (at level 20).
-*)
-
set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
Transparent f_equal.
*)
+(* NOTATION
+Notation Pair := (pair (B:=_)).
+*)
+
+(* NOTATION
+Notation Proj1 := (proj1 (B:=_)).
+*)
+
+(* NOTATION
+Notation Proj2 := (proj2 (B:=_)).
+*)
+
(* Following only needed in finite, but tha's now obsolete
Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
(* 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 *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbGroups".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/CGroups.ma".
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.
set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbMonoids".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/CMonoids.ma".
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.
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 $ *)
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 *)
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].
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.
*)
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 $ *)
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 *)
Implicit Arguments cg_inv [c].
*)
+(* NOTATION
+Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
+*)
+
inline "cic:/CoRN/algebra/CGroups/cg_minus.con".
(*#*
Implicit Arguments cg_minus [G].
*)
+(* NOTATION
+Infix "[-]" := cg_minus (at level 50, left associativity).
+*)
+
(* End_SpecReals *)
(*#*
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.
*)
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 $ *)
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".
(* 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".
(* 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 *)
(*
inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".
+(* NOTATION
+Notation ProjT1 := (proj1_sigT _ _).
+*)
+
+(* NOTATION
+Notation ProjT2 := (proj2_sigT _ _).
+*)
+
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 $ *)
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}%
e.g. for the setoid of non-zeros.
*)
+(* NOTATION
+Notation Zero := (cm_unit _).
+*)
+
inline "cic:/CoRN/algebra/CMonoids/nonZeroP.con".
(* End_SpecReals *)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdAbs".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/COrdFields2.ma".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con".
inline "cic:/CoRN/algebra/COrdAbs/absBig.con".
+(* NOTATION
+Notation AbsBig := (absBig _).
+*)
+
inline "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con".
(* UNEXPORTED
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdCauchy".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/COrdAbs.ma".
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".
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 $ *)
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}%
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 *)
(*#*
Implicit Arguments leEq [F].
*)
+(* NOTATION
+Infix "[<=]" := leEq (at level 70, no associativity).
+*)
+
(* UNEXPORTED
Section COrdField_axioms.
*)
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.
*)
set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields2".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/COrdFields.ma".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:R).
+*)
+
+(* NOTATION
+Notation OneR := (One:R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con".
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 $ *)
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
include "tactics/Transparent_algebra.ma".
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con".
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con".
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 $ *)
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
(*#*
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con".
(* begin hide *)
+(* NOTATION
+Notation FX := (cpoly_cring F).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult.con".
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 $ *)
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
(*#*
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_zero.con".
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 $ *)
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}%
*)
inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+(* NOTATION
+Notation RX := (cpoly_cring CR).
+*)
+
(* UNEXPORTED
Section helpful_section.
*)
Implicit Arguments cpoly_apply_fun [CR].
*)
+(* NOTATION
+Infix "!" := cpoly_apply_fun (at level 1, no associativity).
+*)
+
(*#*
** Basic properties of polynomials
%\begin{convention}%
inline "cic:/CoRN/algebra/CPolynomials/R.var".
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(*#*
*** Constant and identity
*)
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
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 $ *)
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".
inline "cic:/CoRN/algebra/CRings/cr_minus.con".
+(* NOTATION
+Notation One := (cr_one _).
+*)
+
(* End_SpecReals *)
(* Begin_SpecReals *)
Implicit Arguments cr_mult [c].
*)
+(* NOTATION
+Infix "[*]" := cr_mult (at level 40, left associativity).
+*)
+
(* UNEXPORTED
Section CRing_axioms.
*)
(* End_SpecReals *)
+(* NOTATION
+Notation "x [^] n" := (nexp_op _ n x) (at level 20).
+*)
+
(* UNEXPORTED
Implicit Arguments nexp_op [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".
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.
*)
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 $ *)
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}%
Implicit Arguments csg_op [c].
*)
+(* NOTATION
+Infix "[+]" := csg_op (at level 50, left associativity).
+*)
+
(* End_SpecReals *)
(*#* **Semigroup axioms
Implicit Arguments Fplus [G].
*)
+(* NOTATION
+Infix "{+}" := Fplus (at level 50, left associativity).
+*)
+
(* UNEXPORTED
Hint Resolve included_FPlus : included.
*)
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 $ *)
End SubSets_of_G.
*)
+(* NOTATION
+Notation Conj := (conjP _).
+*)
+
(* UNEXPORTED
Implicit Arguments disj [S].
*)
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].
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].
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.
*)
Implicit Arguments conj_wd [S P Q].
*)
+(* NOTATION
+Notation Prj1 := (prj1 _ _ _ _).
+*)
+
+(* NOTATION
+Notation Prj2 := (prj2 _ _ _ _).
+*)
+
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 $ *)
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 $ *)
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].
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".
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
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".
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".
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}%
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".
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".
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".
(* 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 *)
(* 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 *)
(* 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 *)
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
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 $ *)
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 $ *)
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 *)
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]
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 $ *)
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 $ *)
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}%
set "baseuri" "cic:/matita/CoRN-Decl/algebra/ListType".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
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 $ *)
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 $ *)
(* 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
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 $ *)
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 $ *)
set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/IDA/Ch6".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/CSemiGroups.ma".
set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/csetfun".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/CSetoids.ma".
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".
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".
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 $ *)
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".
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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".
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
Implicit Arguments Fprim [I F].
*)
+(* NOTATION
+Notation "[-S-] F" := (Fprim F) (at level 20).
+*)
+
(* UNEXPORTED
Section FTC.
*)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
(* end hide *)
+(* NOTATION
+Notation Integral := (integral _ _ Hab).
+*)
+
(* UNEXPORTED
Section Well_Definedness.
*)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
(* 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 *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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].
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 $ *)
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".
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 *)
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 $ *)
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 $ *)
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".
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 $ *)
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".
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".
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 $ *)
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".
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 $ *)
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 $ *)
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 $ *)
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 *)
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 $ *)
(* begin hide *)
+(* NOTATION
+Infix "**" := prodT (at level 20).
+*)
+
(* end hide *)
include "ftc/Continuity.ma".
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 $ *)
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.
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 $ *)
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 $ *)
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.
Implicit Arguments cms_d [c].
*)
+(* NOTATION
+Infix "[-d]" := cms_d (at level 68, left associativity).
+*)
+
(* UNEXPORTED
Section PsMS_axioms.
*)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
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".
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 $ *)
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 $ *)
End Q.
*)
+(* NOTATION
+Infix "{=Q}" := Qeq (no associativity, at level 90).
+*)
+
+(* NOTATION
+Infix "{#Q}" := Qap (no associativity, at level 90).
+*)
+
+(* NOTATION
+Infix "{<Q}" := Qlt (no associativity, at level 90).
+*)
+
+(* NOTATION
+Infix "{+Q}" := Qplus (no associativity, at level 85).
+*)
+
+(* NOTATION
+Infix "{*Q}" := Qmult (no associativity, at level 80).
+*)
+
+(* NOTATION
+Notation "{-Q}" := Qopp (at level 1, left associativity).
+*)
+
(*#* ***Constants
*)
inline "cic:/CoRN/model/structures/Qsec/inject_Z.con".
-coercion "cic:/matita/CoRN-Decl/model/structures/Qsec/inject_Z.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/model/structures/Qsec/inject_Z.con 0 (* compounds *).
inline "cic:/CoRN/model/structures/Qsec/injz_plus.con".
set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Zsec".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Zsec.v,v 1.5 2004/04/06 15:46:05 lcf Exp $ *)
inline "cic:/CoRN/model/structures/Zsec/ap_Z.con".
+(* NOTATION
+Infix "{#Z}" := ap_Z (no associativity, at level 90).
+*)
+
(*#* Some properties of apartness:
*)
(* begin hide *)
-coercion "cic:/matita/CoRN-Decl/model/structures/Zsec/Zpos.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/model/structures/Zsec/Zpos.con 0 (* compounds *).
(* end hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Bridges_LUB".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
inline "cic:/CoRN/reals/Bridges_LUB/dcotrans_analyze_strong.con".
+(* NOTATION
+Notation "( p , q )" := (pairT p q).
+*)
+
inline "cic:/CoRN/reals/Bridges_LUB/dif_cotrans.con".
inline "cic:/CoRN/reals/Bridges_LUB/dif_cotrans_strong.con".
set "baseuri" "cic:/matita/CoRN-Decl/reals/Bridges_iso".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CMetricFields".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CMetricFields.v,v 1.6 2004/04/23 10:01:03 lcf Exp $ *)
inline "cic:/CoRN/reals/CMetricFields/CMetricField.ind".
-coercion "cic:/matita/CoRN-Decl/reals/CMetricFields/cmf_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/CMetricFields/cmf_crr.con 0 (* compounds *).
(* UNEXPORTED
End CMetric_Fields.
*)
+(* NOTATION
+Notation MAbs := (cmf_abs _).
+*)
+
(* UNEXPORTED
Section basics.
*)
inline "cic:/CoRN/reals/CMetricFields/MCauchySeq.ind".
-coercion "cic:/matita/CoRN-Decl/reals/CMetricFields/MCS_seq.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/CMetricFields/MCS_seq.con 0 (* compounds *).
inline "cic:/CoRN/reals/CMetricFields/MseqLimit.con".
set "baseuri" "cic:/matita/CoRN-Decl/reals/CPoly_Contin".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CPoly_Contin.v,v 1.6 2004/04/23 10:01:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CReals.v,v 1.2 2004/04/05 11:35:38 lcf Exp $ *)
inline "cic:/CoRN/reals/CReals/CReals.ind".
-coercion "cic:/matita/CoRN-Decl/reals/CReals/crl_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/CReals/crl_crr.con 0 (* compounds *).
(* End_SpecReals *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals1".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CReals1.v,v 1.4 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CSumsReals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CSumsReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/CauchySeq".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
inline "cic:/CoRN/reals/CauchySeq/IR.var".
+(* NOTATION
+Notation PartIR := (PartFunct IR).
+*)
+
+(* NOTATION
+Notation ProjIR1 := (prj1 IR _ _ _).
+*)
+
+(* NOTATION
+Notation ProjIR2 := (prj2 IR _ _ _).
+*)
+
include "tactics/Transparent_algebra.ma".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:IR).
+*)
+
+(* NOTATION
+Notation OneR := (One:IR).
+*)
+
(* end hide *)
(* UNEXPORTED
set "baseuri" "cic:/matita/CoRN-Decl/reals/Cauchy_CReals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Cauchy_CReals.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
inline "cic:/CoRN/reals/Cauchy_CReals/F.var".
+(* NOTATION
+Notation "'R_COrdField''" := (R_COrdField F).
+*)
+
inline "cic:/CoRN/reals/Cauchy_CReals/inject_Q.con".
inline "cic:/CoRN/reals/Cauchy_CReals/ing_eq.con".
set "baseuri" "cic:/matita/CoRN-Decl/reals/IVT".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: IVT.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Intervals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Intervals.v,v 1.10 2004/04/23 10:01:04 lcf Exp $ *)
End Intervals.
*)
+(* NOTATION
+Notation Compact := (compact _ _).
+*)
+
(* UNEXPORTED
Implicit Arguments Frestr [F P].
*)
+(* NOTATION
+Notation FRestr := (Frestr (compact_wd _ _ _)).
+*)
+
(* UNEXPORTED
Section More_Intervals.
*)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Max_AbsIR".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Max_AbsIR.v,v 1.13 2004/04/23 10:01:04 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/NRootIR".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/OddPolyRootIR".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: OddPolyRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_dense".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
inline "cic:/CoRN/reals/Q_dense/Interval.ind".
-coercion "cic:/matita/CoRN-Decl/reals/Q_dense/pair_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/Q_dense/pair_crr.con 0 (* compounds *).
inline "cic:/CoRN/reals/Q_dense/Length.con".
inline "cic:/CoRN/reals/Q_dense/trichotomy_strong1.con".
+(* NOTATION
+Notation "( A , B )" := (pairT A B).
+*)
+
inline "cic:/CoRN/reals/Q_dense/if_cotrans.con".
inline "cic:/CoRN/reals/Q_dense/if_cotrans_strong.con".
set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_in_CReals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Q_in_CReals.v,v 1.10 2004/04/23 10:01:05 lcf Exp $ *)
(*#**************************************)
-coercion "cic:/matita/CoRN-Decl/reals/Q_in_CReals/nat_of_P.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/Q_in_CReals/nat_of_P.con 0 (* compounds *).
(* end hide *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/R_morphism".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
inline "cic:/CoRN/reals/R_morphism/Homomorphism.ind".
-coercion "cic:/matita/CoRN-Decl/reals/R_morphism/map.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/reals/R_morphism/map.con 0 (* compounds *).
(* This might be useful later...
Definition Homo_as_CSetoid_fun:=
set "baseuri" "cic:/matita/CoRN-Decl/reals/RealFuncts".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RealFuncts.v,v 1.4 2004/04/07 15:08:10 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/RealLists".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RealLists.v,v 1.4 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/Series".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Series.v,v 1.6 2004/04/23 10:01:05 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/reals/iso_CReals".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/AlgReflection".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: AlgReflection.v,v 1.2 2004/03/26 16:07:03 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics1".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics2".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: DiffTactics2.v,v 1.1.1.1 2004/02/05 16:25:45 lionelm Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics3".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: DiffTactics3.v,v 1.1.1.1 2004/02/05 16:25:44 lionelm Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/FieldReflection".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: FieldReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
inline "cic:/CoRN/tactics/FieldReflection/pfun.var".
+(* NOTATION
+Notation II := (interpF F val unop binop pfun).
+*)
+
(*
four kinds of exprs:
set "baseuri" "cic:/matita/CoRN-Decl/tactics/GroupReflection".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: GroupReflection.v,v 1.3 2004/04/23 10:01:06 lcf Exp $ *)
inline "cic:/CoRN/tactics/GroupReflection/pfun.var".
+(* NOTATION
+Notation II := (interpG G val unop binop pfun).
+*)
+
(*
four kinds of exprs:
set "baseuri" "cic:/matita/CoRN-Decl/tactics/Opaque_algebra".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Opaque_algebra.v,v 1.1 2004/02/11 10:56:57 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/RingReflection".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RingReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
inline "cic:/CoRN/tactics/RingReflection/pfun.var".
+(* NOTATION
+Notation II := (interpR R val unop binop pfun).
+*)
+
(*
four kinds of exprs:
set "baseuri" "cic:/matita/CoRN-Decl/tactics/Step".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* begin hide *)
set "baseuri" "cic:/matita/CoRN-Decl/tactics/Transparent_algebra".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Transparent_algebra.v,v 1.1 2004/02/11 10:56:58 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/Exponential".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Exponential.v,v 1.7 2004/04/23 10:01:07 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/InvTrigonom".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: InvTrigonom.v,v 1.9 2004/04/23 10:01:07 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/Pi".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "transc/SinCos.ma".
set "baseuri" "cic:/matita/CoRN-Decl/transc/PowerSeries".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
set "baseuri" "cic:/matita/CoRN-Decl/transc/RealPowers".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
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
End Power_Function.
*)
+(* NOTATION
+Notation "F {!} G" := (FPower F G) (at level 20).
+*)
+
(* UNEXPORTED
Section More_on_Power_Function.
*)
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 $ *)
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 $ *)
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 $ *)
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 $ *)
projects / helm.git / commitdiff