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