1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/ListType".
23 (*#**********************************************************************)
25 (* v * The Coq Proof Assistant / The Coq Development Team *)
27 (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
29 (* \VV/ *************************************************************)
31 (* // * This file is distributed under the terms of the *)
33 (* * GNU Lesser General Public License Version 2.1 *)
35 (*#**********************************************************************)
37 (*i $Id: ListType.v,v 1.2 2004/03/26 16:07:02 lcf Exp $ i*)
39 (* THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
41 (* Moved to Type for CoRN *)
46 %\cleardoublepage\setcounter{page}{1}%
49 This file contains a variant of the development of lists in the standard
50 library of Coq but moved to the Type level.
57 alias id "A" = "cic:/CoRN/algebra/ListType/List/A.var".
59 inline "cic:/CoRN/algebra/ListType/list.ind".
61 inline "cic:/CoRN/algebra/ListType/app.con".
63 inline "cic:/CoRN/algebra/ListType/app_nil_end.con".
66 Hint Resolve app_nil_end: list v62.
69 inline "cic:/CoRN/algebra/ListType/app_ass.con".
72 Hint Resolve app_ass: list v62.
75 inline "cic:/CoRN/algebra/ListType/ass_app.con".
78 Hint Resolve ass_app: list v62.
81 inline "cic:/CoRN/algebra/ListType/tail.con".
83 inline "cic:/CoRN/algebra/ListType/nil_cons.con".
85 (*#***************************************)
89 (*#***************************************)
91 inline "cic:/CoRN/algebra/ListType/length.con".
93 (*#*****************************)
95 (* Length order of lists *)
97 (*#*****************************)
103 inline "cic:/CoRN/algebra/ListType/lel.con".
106 Hint Unfold lel: list.
109 alias id "a" = "cic:/CoRN/algebra/ListType/List/length_order/a.var".
111 alias id "b" = "cic:/CoRN/algebra/ListType/List/length_order/b.var".
113 alias id "l" = "cic:/CoRN/algebra/ListType/List/length_order/l.var".
115 alias id "m" = "cic:/CoRN/algebra/ListType/List/length_order/m.var".
117 alias id "n" = "cic:/CoRN/algebra/ListType/List/length_order/n.var".
119 inline "cic:/CoRN/algebra/ListType/lel_refl.con".
121 inline "cic:/CoRN/algebra/ListType/lel_trans.con".
123 inline "cic:/CoRN/algebra/ListType/lel_cons_cons.con".
125 inline "cic:/CoRN/algebra/ListType/lel_cons.con".
127 inline "cic:/CoRN/algebra/ListType/lel_tail.con".
129 inline "cic:/CoRN/algebra/ListType/lel_nil.con".
136 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
140 inline "cic:/CoRN/algebra/ListType/In.con".
142 inline "cic:/CoRN/algebra/ListType/in_eq.con".
145 Hint Resolve in_eq: list v62.
148 inline "cic:/CoRN/algebra/ListType/in_cons.con".
151 Hint Resolve in_cons: list v62.
154 inline "cic:/CoRN/algebra/ListType/in_app_or.con".
157 Hint Immediate in_app_or: list v62.
160 inline "cic:/CoRN/algebra/ListType/in_or_app.con".
163 Hint Resolve in_or_app: list v62.
166 inline "cic:/CoRN/algebra/ListType/incl.con".
169 Hint Unfold incl: list v62.
172 inline "cic:/CoRN/algebra/ListType/incl_refl.con".
175 Hint Resolve incl_refl: list v62.
178 inline "cic:/CoRN/algebra/ListType/incl_tl.con".
181 Hint Immediate incl_tl: list v62.
184 inline "cic:/CoRN/algebra/ListType/incl_tran.con".
186 inline "cic:/CoRN/algebra/ListType/incl_appl.con".
189 Hint Immediate incl_appl: list v62.
192 inline "cic:/CoRN/algebra/ListType/incl_appr.con".
195 Hint Immediate incl_appr: list v62.
198 inline "cic:/CoRN/algebra/ListType/incl_cons.con".
201 Hint Resolve incl_cons: list v62.
204 inline "cic:/CoRN/algebra/ListType/incl_app.con".
211 Implicit Arguments length [A].
215 Implicit Arguments In [A].
219 Implicit Arguments cons [A].
226 alias id "A" = "cic:/CoRN/algebra/ListType/Map/A.var".
228 alias id "B" = "cic:/CoRN/algebra/ListType/Map/B.var".
230 alias id "f" = "cic:/CoRN/algebra/ListType/Map/f.var".
232 inline "cic:/CoRN/algebra/ListType/map.con".
239 Implicit Arguments map [A B].
243 Hint Resolve incl_app: list v62.