(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__".
+inline procedural "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__" as definition.
(* end hide *)
alias id "Hf" = "cic:/CoRN/ftc/PartInterval/Conversion/Hf.var".
-inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR.con" as definition.
(* UNEXPORTED
End Conversion
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__".
+inline procedural "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__" as definition.
(* end hide *)
alias id "f" = "cic:/CoRN/ftc/PartInterval/AntiConversion/f.var".
-inline procedural "cic:/CoRN/ftc/PartInterval/PartInt_strext.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/PartInt_strext.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/PartInt.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/PartInt.con" as definition.
(* UNEXPORTED
End AntiConversion
In one direction these operators are inverses.
*)
-inline procedural "cic:/CoRN/ftc/PartInterval/int_part_int.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/int_part_int.con" as lemma.
(* UNEXPORTED
End Inverses
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__".
+inline procedural "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__" as definition.
(* end hide *)
alias id "Gg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var".
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_const.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_const.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_id.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_id.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_plus.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_plus.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_inv.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_inv.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_minus.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_minus.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_mult.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_mult.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_nth.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_nth.con" as lemma.
(* begin show *)
(* end show *)
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_recip.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_recip.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartInterval/part_int_div.con".
+inline procedural "cic:/CoRN/ftc/PartInterval/part_int_div.con" as lemma.
(* UNEXPORTED
End Equivalences