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