matita/contribs/CoRN-Decl/algebra/ListType.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/algebra/ListType".
  18
  19 (* begin hide *)
  20
  21 (*#**********************************************************************)
  22
  23 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
  24
  25 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
  26
  27 (*   \VV/  *************************************************************)
  28
  29 (*    //   *      This file is distributed under the terms of the      *)
  30
  31 (*         *       GNU Lesser General Public License Version 2.1       *)
  32
  33 (*#**********************************************************************)
  34
  35 (*i $Id: ListType.v,v 1.2 2004/03/26 16:07:02 lcf Exp $ i*)
  36
  37 (* THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
  38
  39 (* Moved to Type for CoRN *)
  40
  41 (* end hide *)
  42
  43 (*#*
  44 %\cleardoublepage\setcounter{page}{1}%
  45 *Lists in Type
  46
  47 This file contains a variant of the development of lists in the standard
  48 library of Coq but moved to the Type level.
  49 *)
  50
  51 (* INCLUDE
  52 Le
  53 *)
  54
  55 (* UNEXPORTED
  56 Section List.
  57 *)
  58
  59 inline cic:/CoRN/algebra/ListType/A.var.
  60
  61 inline cic:/CoRN/algebra/ListType/list.ind.
  62
  63 inline cic:/CoRN/algebra/ListType/app.con.
  64
  65 inline cic:/CoRN/algebra/ListType/app_nil_end.con.
  66
  67 (* UNEXPORTED
  68 Hint Resolve app_nil_end: list v62.
  69 *)
  70
  71 inline cic:/CoRN/algebra/ListType/app_ass.con.
  72
  73 (* UNEXPORTED
  74 Hint Resolve app_ass: list v62.
  75 *)
  76
  77 inline cic:/CoRN/algebra/ListType/ass_app.con.
  78
  79 (* UNEXPORTED
  80 Hint Resolve ass_app: list v62.
  81 *)
  82
  83 inline cic:/CoRN/algebra/ListType/tail.con.
  84
  85 inline cic:/CoRN/algebra/ListType/nil_cons.con.
  86
  87 (*#***************************************)
  88
  89 (* Length of lists                      *)
  90
  91 (*#***************************************)
  92
  93 inline cic:/CoRN/algebra/ListType/length.con.
  94
  95 (*#*****************************)
  96
  97 (* Length order of lists      *)
  98
  99 (*#*****************************)
 100
 101 (* UNEXPORTED
 102 Section length_order.
 103 *)
 104
 105 inline cic:/CoRN/algebra/ListType/lel.con.
 106
 107 (* UNEXPORTED
 108 Hint Unfold lel: list.
 109 *)
 110
 111 inline cic:/CoRN/algebra/ListType/a.var.
 112
 113 inline cic:/CoRN/algebra/ListType/b.var.
 114
 115 inline cic:/CoRN/algebra/ListType/l.var.
 116
 117 inline cic:/CoRN/algebra/ListType/m.var.
 118
 119 inline cic:/CoRN/algebra/ListType/n.var.
 120
 121 inline cic:/CoRN/algebra/ListType/lel_refl.con.
 122
 123 inline cic:/CoRN/algebra/ListType/lel_trans.con.
 124
 125 inline cic:/CoRN/algebra/ListType/lel_cons_cons.con.
 126
 127 inline cic:/CoRN/algebra/ListType/lel_cons.con.
 128
 129 inline cic:/CoRN/algebra/ListType/lel_tail.con.
 130
 131 inline cic:/CoRN/algebra/ListType/lel_nil.con.
 132
 133 (* UNEXPORTED
 134 End length_order.
 135 *)
 136
 137 (* UNEXPORTED
 138 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
 139   v62.
 140 *)
 141
 142 inline cic:/CoRN/algebra/ListType/In.con.
 143
 144 inline cic:/CoRN/algebra/ListType/in_eq.con.
 145
 146 (* UNEXPORTED
 147 Hint Resolve in_eq: list v62.
 148 *)
 149
 150 inline cic:/CoRN/algebra/ListType/in_cons.con.
 151
 152 (* UNEXPORTED
 153 Hint Resolve in_cons: list v62.
 154 *)
 155
 156 inline cic:/CoRN/algebra/ListType/in_app_or.con.
 157
 158 (* UNEXPORTED
 159 Hint Immediate in_app_or: list v62.
 160 *)
 161
 162 inline cic:/CoRN/algebra/ListType/in_or_app.con.
 163
 164 (* UNEXPORTED
 165 Hint Resolve in_or_app: list v62.
 166 *)
 167
 168 inline cic:/CoRN/algebra/ListType/incl.con.
 169
 170 (* UNEXPORTED
 171 Hint Unfold incl: list v62.
 172 *)
 173
 174 inline cic:/CoRN/algebra/ListType/incl_refl.con.
 175
 176 (* UNEXPORTED
 177 Hint Resolve incl_refl: list v62.
 178 *)
 179
 180 inline cic:/CoRN/algebra/ListType/incl_tl.con.
 181
 182 (* UNEXPORTED
 183 Hint Immediate incl_tl: list v62.
 184 *)
 185
 186 inline cic:/CoRN/algebra/ListType/incl_tran.con.
 187
 188 inline cic:/CoRN/algebra/ListType/incl_appl.con.
 189
 190 (* UNEXPORTED
 191 Hint Immediate incl_appl: list v62.
 192 *)
 193
 194 inline cic:/CoRN/algebra/ListType/incl_appr.con.
 195
 196 (* UNEXPORTED
 197 Hint Immediate incl_appr: list v62.
 198 *)
 199
 200 inline cic:/CoRN/algebra/ListType/incl_cons.con.
 201
 202 (* UNEXPORTED
 203 Hint Resolve incl_cons: list v62.
 204 *)
 205
 206 inline cic:/CoRN/algebra/ListType/incl_app.con.
 207
 208 (* UNEXPORTED
 209 End List.
 210 *)
 211
 212 (* UNEXPORTED
 213 Implicit Arguments length [A].
 214 *)
 215
 216 (* UNEXPORTED
 217 Implicit Arguments In [A].
 218 *)
 219
 220 (* UNEXPORTED
 221 Implicit Arguments cons [A].
 222 *)
 223
 224 (* UNEXPORTED
 225 Section Map.
 226 *)
 227
 228 inline cic:/CoRN/algebra/ListType/A.var.
 229
 230 inline cic:/CoRN/algebra/ListType/B.var.
 231
 232 inline cic:/CoRN/algebra/ListType/f.var.
 233
 234 inline cic:/CoRN/algebra/ListType/map.con.
 235
 236 (* UNEXPORTED
 237 End Map.
 238 *)
 239
 240 (* UNEXPORTED
 241 Implicit Arguments map [A B].
 242 *)
 243
 244 (* UNEXPORTED
 245 Hint Resolve incl_app: list v62.
 246 *)
 247