1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
9
Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
10
Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
11
Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3.
12
Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4.
13
Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5.
14
Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6.
15
Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7.
16
Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8.
17
Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9.
18
Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10.
19
Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11.
20
Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12.
21
Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13.
22
Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14.
23
Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15.
24
Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16.
25
Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17.
26
Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18.
27
Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19.
28
Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20.
29
Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21.
30
Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22.
31
Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23.
32
Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24.
33
Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25.
34
Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26.
35
Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27.
36
Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28.
37
Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29.
38
Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30.
39
Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31.
40
Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32.
41
Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33.
42
Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34.
43
Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35.
44
Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36.
45
Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37.
46
Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38.
47
Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39.
48
Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40.
49
Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41.
50
Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42.
51
Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43.
52
Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44.
53
Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45.
54
Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46.
55
Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47.
56
Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48.
57
Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49.
58
Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50.
59
Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51.
60
Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52.
61
Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53.
62
Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54.
63
Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55.
64
Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56.
65
Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57.
66
Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58.
67
Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59.
68
Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60.
69
Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61.
70
Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62.
71
Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63.
72
Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64.
73
Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65.
74
Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66.
75
Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67.
76
Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68.
77
Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69.
78
Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70.
79
Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71.
80
Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72.
81
Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73.
82
Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74.
83
Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75.
84
Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76.
85
Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77.
86
Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78.
87
Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79.
88
Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80.
89
Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81.
90
Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82.
91
Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83.
92
Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84.
93
Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85.
94
Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86.
95
Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87.
96
Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88.
97
Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89.
98
Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90.
99
Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91.
100
Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92.
101
Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93.
102
Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94.
103
Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95.
104
Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96.
105
Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97.
106
Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98.
107
Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99.
added
removed
test-suite/bench/lists-100.v
