From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/bench/lists_100.v | 107 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 test-suite/bench/lists_100.v (limited to 'test-suite/bench/lists_100.v') diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v new file mode 100644 index 00000000..4accbf34 --- /dev/null +++ b/test-suite/bench/lists_100.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* list0 -> list0. +Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. +Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. +Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. +Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. +Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. +Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. +Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. +Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. +Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. +Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. +Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. +Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. +Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. +Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. +Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. +Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. +Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. +Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. +Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. +Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. +Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. +Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. +Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. +Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. +Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. +Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. +Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. +Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. +Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. +Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. +Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. +Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. +Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. +Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. +Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. +Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. +Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. +Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. +Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. +Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. +Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. +Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. +Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. +Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. +Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. +Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. +Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. +Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. +Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. +Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. +Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. +Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. +Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. +Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. +Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. +Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. +Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. +Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. +Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. +Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. +Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. +Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. +Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. +Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. +Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. +Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. +Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. +Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. +Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. +Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. +Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. +Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. +Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. +Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. +Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. +Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. +Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. +Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. +Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. +Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. +Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. +Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. +Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. +Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. +Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. +Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. +Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. +Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. +Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. +Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. +Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. +Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. +Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. +Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. +Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. +Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. +Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. +Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. +Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. -- cgit v1.2.3