-
Notifications
You must be signed in to change notification settings - Fork 12
/
_CoqProject
210 lines (201 loc) · 7.41 KB
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
-R theories/ordinals hydras
-R theories/additions additions
-R theories/gaia gaia_hydras
-R theories/goedel Goedel
-R exercises hydra_exercises
-arg -w -arg -notation-overridden
-arg -w -arg -ambiguous-paths
-arg -w -arg -deprecated-hint-rewrite-without-locality
-arg -w -arg -unknown-option
-arg -w -arg -deprecated-option
theories/ordinals/OrdinalNotations/ON_Omega.v
theories/ordinals/OrdinalNotations/ON_Generic.v
theories/ordinals/OrdinalNotations/ON_Finite.v
theories/ordinals/OrdinalNotations/ON_mult.v
theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
theories/ordinals/OrdinalNotations/ON_plus.v
theories/ordinals/OrdinalNotations/ON_O.v
theories/ordinals/OrdinalNotations/ON_Omega2.v
theories/ordinals/OrdinalNotations/Example_3PlusOmega.v
theories/ordinals/OrdinalNotations/OmegaOmega.v
theories/ordinals/Prelude/ssrnat_extracts.v
theories/ordinals/Prelude/MoreDecidable.v
theories/ordinals/Prelude/STDPP_compat.v
theories/ordinals/Prelude/Comparable.v
theories/ordinals/Prelude/First_toggle.v
theories/ordinals/Prelude/Simple_LexProd.v
theories/ordinals/Prelude/DecPreOrder.v
theories/ordinals/Prelude/Exp2.v
theories/ordinals/Prelude/Sort_spec.v
theories/ordinals/Prelude/Merge_Sort.v
theories/ordinals/Prelude/WfVariant.v
theories/ordinals/Prelude/More_Arith.v
theories/ordinals/Prelude/DecPreOrder_Instances.v
theories/ordinals/Prelude/Fuel.v
theories/ordinals/Prelude/Iterates.v
theories/ordinals/Prelude/OrdNotations.v
theories/ordinals/Prelude/MoreLists.v
theories/ordinals/Prelude/Restriction.v
theories/ordinals/Prelude/MoreOrders.v
theories/ordinals/Prelude/MoreVectors.v
theories/ordinals/Prelude/Compat815.v
theories/ordinals/Prelude/MoreLibHyps.v
theories/ordinals/Prelude/LibHyps_Experiments.v
theories/ordinals/Epsilon0/Hessenberg.v
theories/ordinals/Epsilon0/Large_Sets.v
theories/ordinals/Epsilon0/Epsilon0rpo.v
theories/ordinals/Epsilon0/Hprime.v
theories/ordinals/Epsilon0/E0.v
theories/ordinals/Epsilon0/T1.v
theories/ordinals/Epsilon0/Paths.v
theories/ordinals/Epsilon0/Canon.v
theories/ordinals/Epsilon0/Large_Sets_Examples.v
theories/ordinals/Epsilon0/L_alpha.v
theories/ordinals/Epsilon0/Epsilon0.v
theories/ordinals/Epsilon0/F_alpha.v
theories/ordinals/Epsilon0/F_omega.v
theories/ordinals/Gamma0/T2.v
theories/ordinals/Gamma0/Gamma0.v
theories/ordinals/rpo/decidable_set.v
theories/ordinals/rpo/dickson.v
theories/ordinals/rpo/list_set.v
theories/ordinals/rpo/list_permut.v
theories/ordinals/rpo/more_list.v
theories/ordinals/rpo/closure.v
theories/ordinals/rpo/rpo.v
theories/ordinals/rpo/term.v
theories/ordinals/Schutte/MoreEpsilonIota.v
theories/ordinals/Schutte/CNF.v
theories/ordinals/Schutte/AP.v
theories/ordinals/Schutte/Schutte_basics.v
theories/ordinals/Schutte/Ordering_Functions.v
theories/ordinals/Schutte/Countable.v
theories/ordinals/Schutte/Critical.v
theories/ordinals/Schutte/Schutte.v
theories/ordinals/Schutte/Well_Orders.v
theories/ordinals/Schutte/Addition.v
theories/ordinals/Schutte/Correctness_E0.v
theories/ordinals/Schutte/PartialFun.v
theories/ordinals/Schutte/Lub.v
theories/ordinals/Schutte/GRelations.v
theories/ordinals/Hydra/Battle_length.v
theories/ordinals/Hydra/Omega_Small.v
theories/ordinals/Hydra/BigBattle.v
theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
theories/ordinals/Hydra/Hydra_Extraction.v
theories/ordinals/Hydra/KP_example.v
theories/ordinals/Hydra/Hydra_Termination.v
theories/ordinals/Hydra/Hydra_Theorems.v
theories/ordinals/Hydra/Omega2_Small.v
theories/ordinals/Hydra/Hydra_Definitions.v
theories/ordinals/Hydra/Epsilon0_Needed_Free.v
theories/ordinals/Hydra/Hydra_Examples.v
theories/ordinals/Hydra/Hydra_Lemmas.v
theories/ordinals/Hydra/O2H.v
theories/ordinals/Hydra/Epsilon0_Needed_Std.v
theories/ordinals/Ackermann/codeNatToTerm.v
theories/ordinals/Ackermann/code.v
theories/ordinals/Ackermann/extEqualNat.v
theories/ordinals/Ackermann/folLogic.v
theories/ordinals/Ackermann/fol.v
theories/ordinals/Ackermann/LNN.v
theories/ordinals/Ackermann/NN2PA.v
theories/ordinals/Ackermann/PAtheory.v
theories/ordinals/Ackermann/prLogic.v
theories/ordinals/Ackermann/wellFormed.v
theories/ordinals/Ackermann/checkPrf.v
theories/ordinals/Ackermann/codePA.v
theories/ordinals/Ackermann/cPair.v
theories/ordinals/Ackermann/folProof.v
theories/ordinals/Ackermann/Languages.v
theories/ordinals/Ackermann/LNT.v
theories/ordinals/Ackermann/NNtheory.v
theories/ordinals/Ackermann/PA.v
theories/ordinals/Ackermann/subAll.v
theories/ordinals/Ackermann/codeFreeVar.v
theories/ordinals/Ackermann/codeSubFormula.v
theories/ordinals/Ackermann/Deduction.v
theories/ordinals/Ackermann/folLogic2.v
theories/ordinals/Ackermann/folProp.v
theories/ordinals/Ackermann/ListExt.v
theories/ordinals/Ackermann/misc.v
theories/ordinals/Ackermann/NN.v
theories/ordinals/Ackermann/subProp.v
theories/ordinals/Ackermann/codeList.v
theories/ordinals/Ackermann/codeSubTerm.v
theories/ordinals/Ackermann/expressible.v
theories/ordinals/Ackermann/folLogic3.v
theories/ordinals/Ackermann/folReplace.v
theories/ordinals/Ackermann/LNN2LNT.v
theories/ordinals/Ackermann/model.v
theories/ordinals/Ackermann/PAconsistent.v
theories/ordinals/Ackermann/primRec.v
theories/ordinals/Ackermann/wConsistent.v
theories/ordinals/Ackermann/NewNotations.v
theories/ordinals/MoreAck/Ack.v
theories/ordinals/MoreAck/AckNotPR.v
theories/ordinals/MoreAck/FolExamples.v
theories/ordinals/MoreAck/Iterate_compat.v
theories/ordinals/MoreAck/PrimRecExamples.v
theories/ordinals/MoreAck/LNN_Examples.v
theories/ordinals/MoreAck/BadSubst.v
theories/ordinals/MoreAck/expressibleExamples.v
theories/ordinals/solutions_exercises/MinPR.v
theories/ordinals/solutions_exercises/MinPR2.v
theories/ordinals/solutions_exercises/FibonacciPR.v
theories/ordinals/solutions_exercises/MorePRExamples.v
theories/ordinals/solutions_exercises/isqrt.v
theories/ordinals/solutions_exercises/T1_ltNotWf.v
theories/ordinals/solutions_exercises/predSuccUnicity.v
theories/ordinals/solutions_exercises/lt_succ_le.v
theories/ordinals/solutions_exercises/Limit_Infinity.v
theories/ordinals/solutions_exercises/ge_omega_iff.v
theories/ordinals/solutions_exercises/schutte_cnf_counter_example.v
theories/ordinals/solutions_exercises/F_3.v
theories/ordinals/solutions_exercises/is_F_monotonous.v
theories/ordinals/solutions_exercises/MultisetWf.v
theories/ordinals/solutions_exercises/OnCodeList.v
theories/additions/AM.v
theories/additions/Addition_Chains.v
theories/additions/BinaryStrat.v
theories/additions/Compatibility.v
theories/additions/Demo.v
theories/additions/Demo_power.v
theories/additions/Dichotomy.v
theories/additions/Euclidean_Chains.v
theories/additions/fib.v
theories/additions/Fib2.v
theories/additions/FirstSteps.v
theories/additions/Monoid_def.v
theories/additions/Monoid_instances.v
theories/additions/More_on_positive.v
theories/additions/Naive.v
theories/additions/Pow.v
theories/additions/Pow_variant.v
theories/additions/Strategies.v
theories/additions/Trace_exercise.v
theories/additions/Wf_transparent.v
theories/gaia/T1Bridge.v
theories/gaia/GaiaToHydra.v
theories/gaia/nfwfgaia.v
theories/gaia/GCanon.v
theories/gaia/GF_alpha.v
theories/gaia/GL_alpha.v
theories/gaia/GHprime.v
theories/gaia/ON_gfinite.v
theories/gaia/GPaths.v
theories/gaia/GLarge_Sets.v
theories/gaia/GHessenberg.v
theories/gaia/HydraGaia_Examples.v
theories/gaia/GHydra.v
theories/gaia/T2Bridge.v
theories/gaia/GPrelude.v
theories/gaia/T1Choice.v
theories/gaia/onType.v
theories/goedel/rosser.v
theories/goedel/goedel1.v
theories/goedel/PRrepresentable.v
theories/goedel/fixPoint.v
theories/goedel/codeSysPrf.v
theories/goedel/rosserPA.v
theories/goedel/goedel2.v