include "ftc/IntervalFunct.ma".
(* UNEXPORTED
-Section Conversion.
+Section Conversion
*)
(*#* *Correspondence
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/PartInterval/F.var".
+alias id "F" = "cic:/CoRN/ftc/PartInterval/Conversion/F.var".
-inline "cic:/CoRN/ftc/PartInterval/a.var".
+alias id "a" = "cic:/CoRN/ftc/PartInterval/Conversion/a.var".
-inline "cic:/CoRN/ftc/PartInterval/b.var".
+alias id "b" = "cic:/CoRN/ftc/PartInterval/Conversion/b.var".
-inline "cic:/CoRN/ftc/PartInterval/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Conversion/Hab.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/PartInterval/I.con".
+inline "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__".
(* end hide *)
-inline "cic:/CoRN/ftc/PartInterval/Hf.var".
+alias id "Hf" = "cic:/CoRN/ftc/PartInterval/Conversion/Hf.var".
inline "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con".
inline "cic:/CoRN/ftc/PartInterval/IntPartIR.con".
(* UNEXPORTED
-End Conversion.
+End Conversion
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section AntiConversion.
+Section AntiConversion
*)
(*#*
domain [[a,b]] and build the corresponding partial function.
*)
-inline "cic:/CoRN/ftc/PartInterval/a.var".
+alias id "a" = "cic:/CoRN/ftc/PartInterval/AntiConversion/a.var".
-inline "cic:/CoRN/ftc/PartInterval/b.var".
+alias id "b" = "cic:/CoRN/ftc/PartInterval/AntiConversion/b.var".
-inline "cic:/CoRN/ftc/PartInterval/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/PartInterval/I.con".
+inline "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__".
(* end hide *)
-inline "cic:/CoRN/ftc/PartInterval/f.var".
+alias id "f" = "cic:/CoRN/ftc/PartInterval/AntiConversion/f.var".
inline "cic:/CoRN/ftc/PartInterval/PartInt_strext.con".
inline "cic:/CoRN/ftc/PartInterval/PartInt.con".
(* UNEXPORTED
-End AntiConversion.
+End AntiConversion
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Inverses.
+Section Inverses
*)
(*#*
inline "cic:/CoRN/ftc/PartInterval/int_part_int.con".
(* UNEXPORTED
-End Inverses.
+End Inverses
*)
(* UNEXPORTED
-Section Equivalences.
+Section Equivalences
*)
(*#* **Mappings Preserve Operations
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/PartInterval/F.var".
+alias id "F" = "cic:/CoRN/ftc/PartInterval/Equivalences/F.var".
-inline "cic:/CoRN/ftc/PartInterval/G.var".
+alias id "G" = "cic:/CoRN/ftc/PartInterval/Equivalences/G.var".
-inline "cic:/CoRN/ftc/PartInterval/a.var".
+alias id "a" = "cic:/CoRN/ftc/PartInterval/Equivalences/a.var".
-inline "cic:/CoRN/ftc/PartInterval/b.var".
+alias id "b" = "cic:/CoRN/ftc/PartInterval/Equivalences/b.var".
-inline "cic:/CoRN/ftc/PartInterval/c.var".
+alias id "c" = "cic:/CoRN/ftc/PartInterval/Equivalences/c.var".
-inline "cic:/CoRN/ftc/PartInterval/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/PartInterval/I.con".
+inline "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__".
(* end hide *)
-inline "cic:/CoRN/ftc/PartInterval/f.var".
+alias id "f" = "cic:/CoRN/ftc/PartInterval/Equivalences/f.var".
-inline "cic:/CoRN/ftc/PartInterval/g.var".
+alias id "g" = "cic:/CoRN/ftc/PartInterval/Equivalences/g.var".
-inline "cic:/CoRN/ftc/PartInterval/Ff.var".
+alias id "Ff" = "cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var".
-inline "cic:/CoRN/ftc/PartInterval/Gg.var".
+alias id "Gg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var".
inline "cic:/CoRN/ftc/PartInterval/part_int_const.con".
(* begin show *)
-inline "cic:/CoRN/ftc/PartInterval/HG.var".
+alias id "HG" = "cic:/CoRN/ftc/PartInterval/Equivalences/HG.var".
-inline "cic:/CoRN/ftc/PartInterval/Hg.var".
+alias id "Hg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var".
(* end show *)
inline "cic:/CoRN/ftc/PartInterval/part_int_div.con".
(* UNEXPORTED
-End Equivalences.
+End Equivalences
*)