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