*)
(* UNEXPORTED
-Section CPoly_CRing.
+Section CPoly_CRing
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var".
(*#*
The intuition behind the type [cpoly] is the following
in terms of these generators.
*)
-inline "cic:/CoRN/algebra/CPolynomials/cpoly_zero_cs.con".
+inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__".
-inline "cic:/CoRN/algebra/CPolynomials/cpoly_linear_cs.con".
+inline "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__".
inline "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con".
inline "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con".
(* UNEXPORTED
-End CPoly_CRing.
+End CPoly_CRing
*)
(* UNEXPORTED
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}%
*)
(* UNEXPORTED
-Section CPoly_CRing_ctd.
+Section CPoly_CRing_ctd
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var".
+
+(* NOTATION
+Notation RX := (cpoly_cring CR).
+*)
(* UNEXPORTED
-Section helpful_section.
+Section helpful_section
*)
-inline "cic:/CoRN/algebra/CPolynomials/p.var".
+alias id "p" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var".
-inline "cic:/CoRN/algebra/CPolynomials/q.var".
+alias id "q" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var".
-inline "cic:/CoRN/algebra/CPolynomials/c.var".
+alias id "c" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var".
-inline "cic:/CoRN/algebra/CPolynomials/d.var".
+alias id "d" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var".
inline "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con".
inline "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con".
(* UNEXPORTED
-End helpful_section.
+End helpful_section
*)
inline "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con".
inline "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con".
(* UNEXPORTED
-End CPoly_CRing_ctd.
+End CPoly_CRing_ctd
*)
(*#*
Implicit Arguments cpoly_apply_fun [CR].
*)
+(* NOTATION
+Infix "!" := cpoly_apply_fun (at level 1, no associativity).
+*)
+
(*#*
** Basic properties of polynomials
%\begin{convention}%
*)
(* UNEXPORTED
-Section Poly_properties.
+Section Poly_properties
*)
-inline "cic:/CoRN/algebra/CPolynomials/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var".
+
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
(*#*
*** Constant and identity
inline "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con".
(* UNEXPORTED
-End Poly_properties.
+End Poly_properties
*)
(*#* ** Induction properties of polynomials for [Prop]
*)
(* UNEXPORTED
-Section Poly_Prop_Induction.
+Section Poly_Prop_Induction
*)
-inline "cic:/CoRN/algebra/CPolynomials/CR.var".
+alias id "CR" = "cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/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
-End Poly_Prop_Induction.
+End Poly_Prop_Induction
*)
(* UNEXPORTED