matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/fta/CPoly_Rev".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CPoly_Rev.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
  22
  23 include "algebra/CPoly_Degree.ma".
  24
  25 (*#* * Reverse of polynomials
  26 *)
  27
  28 (* UNEXPORTED
  29 Section Monomials
  30 *)
  31
  32 (*#*
  33 %\begin{convention}% Let [R] be a ring, and let [RX] be the
  34 polynomials over this ring.
  35 %\end{convention}%
  36 *)
  37
  38 alias id "R" = "cic:/CoRN/fta/CPoly_Rev/Monomials/R.var".
  39
  40 (* begin hide *)
  41
  42 inline "cic:/CoRN/fta/CPoly_Rev/Monomials/RX.con" "Monomials__".
  43
  44 (* end hide *)
  45
  46 inline "cic:/CoRN/fta/CPoly_Rev/monom.con".
  47
  48 inline "cic:/CoRN/fta/CPoly_Rev/monom_coeff.con".
  49
  50 inline "cic:/CoRN/fta/CPoly_Rev/monom_coeff'.con".
  51
  52 (* UNEXPORTED
  53 Hint Resolve monom_coeff monom_coeff': algebra.
  54 *)
  55
  56 inline "cic:/CoRN/fta/CPoly_Rev/monom_degree.con".
  57
  58 inline "cic:/CoRN/fta/CPoly_Rev/monom_S.con".
  59
  60 (* UNEXPORTED
  61 Hint Resolve monom_S: algebra.
  62 *)
  63
  64 inline "cic:/CoRN/fta/CPoly_Rev/monom_wd_lft.con".
  65
  66 (* UNEXPORTED
  67 Hint Resolve monom_wd_lft: algebra_c.
  68 *)
  69
  70 inline "cic:/CoRN/fta/CPoly_Rev/monom_mult'.con".
  71
  72 (* UNEXPORTED
  73 Hint Resolve monom_mult': algebra.
  74 *)
  75
  76 inline "cic:/CoRN/fta/CPoly_Rev/monom_mult.con".
  77
  78 inline "cic:/CoRN/fta/CPoly_Rev/monom_sum.con".
  79
  80 (* UNEXPORTED
  81 End Monomials
  82 *)
  83
  84 (* UNEXPORTED
  85 Hint Resolve monom_coeff monom_coeff' monom_mult monom_sum: algebra.
  86 *)
  87
  88 (* UNEXPORTED
  89 Implicit Arguments monom [R].
  90 *)
  91
  92 (* UNEXPORTED
  93 Section Poly_Reverse
  94 *)
  95
  96 alias id "R" = "cic:/CoRN/fta/CPoly_Rev/Poly_Reverse/R.var".
  97
  98 (* begin hide *)
  99
 100 inline "cic:/CoRN/fta/CPoly_Rev/Poly_Reverse/RX.con" "Poly_Reverse__".
 101
 102 (* end hide *)
 103
 104 inline "cic:/CoRN/fta/CPoly_Rev/Rev.con".
 105
 106 inline "cic:/CoRN/fta/CPoly_Rev/Rev_coeff.con".
 107
 108 inline "cic:/CoRN/fta/CPoly_Rev/Rev_coeff'.con".
 109
 110 (* UNEXPORTED
 111 Hint Resolve Rev_coeff Rev_coeff': algebra.
 112 *)
 113
 114 inline "cic:/CoRN/fta/CPoly_Rev/Rev_wd.con".
 115
 116 (* UNEXPORTED
 117 Hint Resolve Rev_wd: algebra_c.
 118 *)
 119
 120 inline "cic:/CoRN/fta/CPoly_Rev/Rev_rev.con".
 121
 122 (* UNEXPORTED
 123 Hint Resolve Rev_rev: algebra.
 124 *)
 125
 126 inline "cic:/CoRN/fta/CPoly_Rev/Rev_degree_le.con".
 127
 128 inline "cic:/CoRN/fta/CPoly_Rev/Rev_degree.con".
 129
 130 inline "cic:/CoRN/fta/CPoly_Rev/Rev_monom.con".
 131
 132 (* UNEXPORTED
 133 Hint Resolve Rev_monom: algebra.
 134 *)
 135
 136 inline "cic:/CoRN/fta/CPoly_Rev/Rev_zero.con".
 137
 138 (* UNEXPORTED
 139 Hint Resolve Rev_zero: algebra.
 140 *)
 141
 142 inline "cic:/CoRN/fta/CPoly_Rev/Rev_plus.con".
 143
 144 (* UNEXPORTED
 145 Hint Resolve Rev_plus: algebra.
 146 *)
 147
 148 inline "cic:/CoRN/fta/CPoly_Rev/Rev_minus.con".
 149
 150 (* UNEXPORTED
 151 Hint Resolve Rev_minus: algebra.
 152 *)
 153
 154 inline "cic:/CoRN/fta/CPoly_Rev/Rev_sum0.con".
 155
 156 (* UNEXPORTED
 157 Hint Resolve Rev_sum0: algebra.
 158 *)
 159
 160 inline "cic:/CoRN/fta/CPoly_Rev/Rev_sum.con".
 161
 162 inline "cic:/CoRN/fta/CPoly_Rev/Rev_mult.con".
 163
 164 (* UNEXPORTED
 165 End Poly_Reverse
 166 *)
 167
 168 (* UNEXPORTED
 169 Hint Resolve Rev_wd: algebra_c.
 170 *)
 171
 172 (* UNEXPORTED
 173 Hint Resolve Rev_rev Rev_mult: algebra.
 174 *)
 175
 176 (* UNEXPORTED
 177 Implicit Arguments Rev [R].
 178 *)
 179