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
*)
(* UNEXPORTED
-Section CSemiGroup_axioms.
+Section CSemiGroup_axioms
*)
-inline "cic:/CoRN/algebra/CSemiGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSemiGroups/CSemiGroup_axioms/G.var".
inline "cic:/CoRN/algebra/CSemiGroups/CSemiGroup_is_CSemiGroup.con".
inline "cic:/CoRN/algebra/CSemiGroups/plus_assoc.con".
(* UNEXPORTED
-End CSemiGroup_axioms.
+End CSemiGroup_axioms
*)
(* Begin_SpecReals *)
*)
(* UNEXPORTED
-Section CSemiGroup_basics.
+Section CSemiGroup_basics
*)
-inline "cic:/CoRN/algebra/CSemiGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSemiGroups/CSemiGroup_basics/G.var".
(* End_SpecReals *)
inline "cic:/CoRN/algebra/CSemiGroups/plus_assoc_unfolded.con".
(* UNEXPORTED
-End CSemiGroup_basics.
+End CSemiGroup_basics
*)
(* End_SpecReals *)
*)
(* UNEXPORTED
-Section Part_Function_Plus.
+Section Part_Function_Plus
*)
-inline "cic:/CoRN/algebra/CSemiGroups/G.var".
+alias id "G" = "cic:/CoRN/algebra/CSemiGroups/Part_Function_Plus/G.var".
-inline "cic:/CoRN/algebra/CSemiGroups/F.var".
+alias id "F" = "cic:/CoRN/algebra/CSemiGroups/Part_Function_Plus/F.var".
-inline "cic:/CoRN/algebra/CSemiGroups/F'.var".
+alias id "F'" = "cic:/CoRN/algebra/CSemiGroups/Part_Function_Plus/F'.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CSemiGroups/P.con".
+inline "cic:/CoRN/algebra/CSemiGroups/Part_Function_Plus/P.con" "Part_Function_Plus__".
-inline "cic:/CoRN/algebra/CSemiGroups/Q.con".
+inline "cic:/CoRN/algebra/CSemiGroups/Part_Function_Plus/Q.con" "Part_Function_Plus__".
(* end hide *)
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CSemiGroups/R.var".
+alias id "R" = "cic:/CoRN/algebra/CSemiGroups/Part_Function_Plus/R.var".
inline "cic:/CoRN/algebra/CSemiGroups/included_FPlus.con".
inline "cic:/CoRN/algebra/CSemiGroups/included_FPlus''.con".
(* UNEXPORTED
-End Part_Function_Plus.
+End Part_Function_Plus
*)
(* UNEXPORTED
Implicit Arguments Fplus [G].
*)
+(* NOTATION
+Infix "{+}" := Fplus (at level 50, left associativity).
+*)
+
(* UNEXPORTED
Hint Resolve included_FPlus : included.
*)
*)
(* UNEXPORTED
-Section SubCSemiGroups.
+Section SubCSemiGroups
*)
-inline "cic:/CoRN/algebra/CSemiGroups/csg.var".
+alias id "csg" = "cic:/CoRN/algebra/CSemiGroups/SubCSemiGroups/csg.var".
-inline "cic:/CoRN/algebra/CSemiGroups/P.var".
+alias id "P" = "cic:/CoRN/algebra/CSemiGroups/SubCSemiGroups/P.var".
-inline "cic:/CoRN/algebra/CSemiGroups/op_pres_P.var".
+alias id "op_pres_P" = "cic:/CoRN/algebra/CSemiGroups/SubCSemiGroups/op_pres_P.var".
-inline "cic:/CoRN/algebra/CSemiGroups/subcrr.con".
+inline "cic:/CoRN/algebra/CSemiGroups/SubCSemiGroups/subcrr.con" "SubCSemiGroups__".
inline "cic:/CoRN/algebra/CSemiGroups/Build_SubCSemiGroup.con".
(* UNEXPORTED
-End SubCSemiGroups.
+End SubCSemiGroups
*)