helm/software/matita/contribs/procedural/CoRN/algebra/ListType.mma

   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 include "CoRN.ma".
  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 (* UNEXPORTED
  52 Section List
  53 *)
  54
  55 (* UNEXPORTED
  56 cic:/CoRN/algebra/ListType/List/A.var
  57 *)
  58
  59 inline procedural "cic:/CoRN/algebra/ListType/list.ind".
  60
  61 inline procedural "cic:/CoRN/algebra/ListType/app.con" as definition.
  62
  63 inline procedural "cic:/CoRN/algebra/ListType/app_nil_end.con" as lemma.
  64
  65 (* UNEXPORTED
  66 Hint Resolve app_nil_end: list v62.
  67 *)
  68
  69 inline procedural "cic:/CoRN/algebra/ListType/app_ass.con" as lemma.
  70
  71 (* UNEXPORTED
  72 Hint Resolve app_ass: list v62.
  73 *)
  74
  75 inline procedural "cic:/CoRN/algebra/ListType/ass_app.con" as lemma.
  76
  77 (* UNEXPORTED
  78 Hint Resolve ass_app: list v62.
  79 *)
  80
  81 inline procedural "cic:/CoRN/algebra/ListType/tail.con" as definition.
  82
  83 inline procedural "cic:/CoRN/algebra/ListType/nil_cons.con" as lemma.
  84
  85 (*#***************************************)
  86
  87 (* Length of lists                      *)
  88
  89 (*#***************************************)
  90
  91 inline procedural "cic:/CoRN/algebra/ListType/length.con" as definition.
  92
  93 (*#*****************************)
  94
  95 (* Length order of lists      *)
  96
  97 (*#*****************************)
  98
  99 (* UNEXPORTED
 100 Section length_order
 101 *)
 102
 103 inline procedural "cic:/CoRN/algebra/ListType/lel.con" as definition.
 104
 105 (* UNEXPORTED
 106 Hint Unfold lel: list.
 107 *)
 108
 109 (* UNEXPORTED
 110 cic:/CoRN/algebra/ListType/List/length_order/a.var
 111 *)
 112
 113 (* UNEXPORTED
 114 cic:/CoRN/algebra/ListType/List/length_order/b.var
 115 *)
 116
 117 (* UNEXPORTED
 118 cic:/CoRN/algebra/ListType/List/length_order/l.var
 119 *)
 120
 121 (* UNEXPORTED
 122 cic:/CoRN/algebra/ListType/List/length_order/m.var
 123 *)
 124
 125 (* UNEXPORTED
 126 cic:/CoRN/algebra/ListType/List/length_order/n.var
 127 *)
 128
 129 inline procedural "cic:/CoRN/algebra/ListType/lel_refl.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/algebra/ListType/lel_trans.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/algebra/ListType/lel_cons_cons.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/algebra/ListType/lel_cons.con" as lemma.
 136
 137 inline procedural "cic:/CoRN/algebra/ListType/lel_tail.con" as lemma.
 138
 139 inline procedural "cic:/CoRN/algebra/ListType/lel_nil.con" as lemma.
 140
 141 (* UNEXPORTED
 142 End length_order
 143 *)
 144
 145 (* UNEXPORTED
 146 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
 147   v62.
 148 *)
 149
 150 inline procedural "cic:/CoRN/algebra/ListType/In.con" as definition.
 151
 152 inline procedural "cic:/CoRN/algebra/ListType/in_eq.con" as lemma.
 153
 154 (* UNEXPORTED
 155 Hint Resolve in_eq: list v62.
 156 *)
 157
 158 inline procedural "cic:/CoRN/algebra/ListType/in_cons.con" as lemma.
 159
 160 (* UNEXPORTED
 161 Hint Resolve in_cons: list v62.
 162 *)
 163
 164 inline procedural "cic:/CoRN/algebra/ListType/in_app_or.con" as lemma.
 165
 166 (* UNEXPORTED
 167 Hint Immediate in_app_or: list v62.
 168 *)
 169
 170 inline procedural "cic:/CoRN/algebra/ListType/in_or_app.con" as lemma.
 171
 172 (* UNEXPORTED
 173 Hint Resolve in_or_app: list v62.
 174 *)
 175
 176 inline procedural "cic:/CoRN/algebra/ListType/incl.con" as definition.
 177
 178 (* UNEXPORTED
 179 Hint Unfold incl: list v62.
 180 *)
 181
 182 inline procedural "cic:/CoRN/algebra/ListType/incl_refl.con" as lemma.
 183
 184 (* UNEXPORTED
 185 Hint Resolve incl_refl: list v62.
 186 *)
 187
 188 inline procedural "cic:/CoRN/algebra/ListType/incl_tl.con" as lemma.
 189
 190 (* UNEXPORTED
 191 Hint Immediate incl_tl: list v62.
 192 *)
 193
 194 inline procedural "cic:/CoRN/algebra/ListType/incl_tran.con" as lemma.
 195
 196 inline procedural "cic:/CoRN/algebra/ListType/incl_appl.con" as lemma.
 197
 198 (* UNEXPORTED
 199 Hint Immediate incl_appl: list v62.
 200 *)
 201
 202 inline procedural "cic:/CoRN/algebra/ListType/incl_appr.con" as lemma.
 203
 204 (* UNEXPORTED
 205 Hint Immediate incl_appr: list v62.
 206 *)
 207
 208 inline procedural "cic:/CoRN/algebra/ListType/incl_cons.con" as lemma.
 209
 210 (* UNEXPORTED
 211 Hint Resolve incl_cons: list v62.
 212 *)
 213
 214 inline procedural "cic:/CoRN/algebra/ListType/incl_app.con" as lemma.
 215
 216 (* UNEXPORTED
 217 End List
 218 *)
 219
 220 (* UNEXPORTED
 221 Implicit Arguments length [A].
 222 *)
 223
 224 (* UNEXPORTED
 225 Implicit Arguments In [A].
 226 *)
 227
 228 (* UNEXPORTED
 229 Implicit Arguments cons [A].
 230 *)
 231
 232 (* UNEXPORTED
 233 Section Map
 234 *)
 235
 236 (* UNEXPORTED
 237 cic:/CoRN/algebra/ListType/Map/A.var
 238 *)
 239
 240 (* UNEXPORTED
 241 cic:/CoRN/algebra/ListType/Map/B.var
 242 *)
 243
 244 (* UNEXPORTED
 245 cic:/CoRN/algebra/ListType/Map/f.var
 246 *)
 247
 248 inline procedural "cic:/CoRN/algebra/ListType/map.con" as definition.
 249
 250 (* UNEXPORTED
 251 End Map
 252 *)
 253
 254 (* UNEXPORTED
 255 Implicit Arguments map [A B].
 256 *)
 257
 258 (* UNEXPORTED
 259 Hint Resolve incl_app: list v62.
 260 *)
 261