-
Notifications
You must be signed in to change notification settings - Fork 22
/
_CoqProject
194 lines (193 loc) · 7.32 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
-R . coqart
undeprecate/SRC/OldArith.v
ch9_function_specification/SRC/fib_positive.v
ch9_function_specification/SRC/fib_ind.v
ch9_function_specification/SRC/extract.v
ch9_function_specification/SRC/even_odd.v
ch9_function_specification/SRC/exo_eqdec.v
ch9_function_specification/SRC/plus_prim.v
ch9_function_specification/SRC/div2_mod2.v
ch9_function_specification/SRC/mod2.v
ch9_function_specification/SRC/div3.v
ch9_function_specification/SRC/fib_tail.v
ch9_function_specification/SRC/sqrt.v
ch9_function_specification/SRC/plusss.v
ch9_function_specification/SRC/compare_spec.v
ch9_function_specification/SRC/moreperms.v
ch9_function_specification/SRC/chap9.v
ch9_function_specification/SRC/fib_intro.v
ch9_function_specification/SRC/div2tofib_ind.v
ch10_extraction_and_imperative_programs/SRC/chap10.v
ch3_propositions_proofs/SRC/cut_example.v
ch3_propositions_proofs/SRC/chap3.v
ch3_propositions_proofs/SRC/simple_proofs.v
tutorial_type_classes/SRC/Monoid.v
tutorial_type_classes/SRC/Lost_in_NY.v
tutorial_type_classes/SRC/EMonoid.v
tutorial_type_classes/SRC/Monoid_prog.v
tutorial_type_classes/SRC/Power_mono.v
tutorial_type_classes/SRC/Mat.v
tutorial_type_classes/SRC/Trace_Monoid.v
tutorial_type_classes/SRC/Monoid_op_classes.v
ch11_search_trees/SRC/searchtrees2.v
ch11_search_trees/SRC/search_set.v
ch11_search_trees/SRC/chap11.v
tutorial_inductive_co_inductive_types/SRC/RecTutorial.v
ch15_general_recursion/SRC/parsing4.v
ch15_general_recursion/SRC/div_it_companion2.v
ch15_general_recursion/SRC/fib_log.v
ch15_general_recursion/SRC/cubic.v
ch15_general_recursion/SRC/not_decreasing.v
ch15_general_recursion/SRC/log_domain_well_spec.v
ch15_general_recursion/SRC/bdiv.v
ch15_general_recursion/SRC/log2_it.v
ch15_general_recursion/SRC/log2_function.v
ch15_general_recursion/SRC/sqrt.v
ch15_general_recursion/SRC/inclusionwf.v
ch15_general_recursion/SRC/exo_15_14.v
ch15_general_recursion/SRC/log2.v
ch15_general_recursion/SRC/factZ.v
ch15_general_recursion/SRC/factZ_it.v
ch15_general_recursion/SRC/bdivspec.v
ch15_general_recursion/SRC/sqrt_nat_wf.v
ch15_general_recursion/SRC/chap15.v
ch15_general_recursion/SRC/forloops.v
ch15_general_recursion/SRC/exo_15_13.v
ch15_general_recursion/SRC/merge.v
ch15_general_recursion/SRC/btreewf.v
ch15_general_recursion/SRC/sqrt_compute.v
ch14_fundations_of_inductive_types/SRC/factor.v
ch14_fundations_of_inductive_types/SRC/chap14.v
ch14_fundations_of_inductive_types/SRC/update_eq.v
ch14_fundations_of_inductive_types/SRC/ltree_to_ntree.v
ch14_fundations_of_inductive_types/SRC/use_le_ind_max.v
ch14_fundations_of_inductive_types/SRC/ltree_count.v
ch14_fundations_of_inductive_types/SRC/plus_with_natrec.v
ch14_fundations_of_inductive_types/SRC/triangular.v
ch14_fundations_of_inductive_types/SRC/list_ltree_ind2.v
ch14_fundations_of_inductive_types/SRC/triangular_dep.v
ch5_everydays_logic/SRC/exo_on_ex.v
ch5_everydays_logic/SRC/fol.v
ch5_everydays_logic/SRC/class.v
ch5_everydays_logic/SRC/eq_trans.v
ch5_everydays_logic/SRC/plus_permute2.v
ch5_everydays_logic/SRC/impred_not.v
ch5_everydays_logic/SRC/impred.v
ch5_everydays_logic/SRC/on_negation.v
ch5_everydays_logic/SRC/chap5.v
ch5_everydays_logic/SRC/one_four.v
ch5_everydays_logic/SRC/intuitionism.v
ch5_everydays_logic/SRC/my_le.v
ch5_everydays_logic/SRC/leibniz_with_classes.v
ch5_everydays_logic/SRC/dyslexia.v
ch5_everydays_logic/SRC/leibniz.v
ch2_types_expressions/SRC/ex1.v
ch2_types_expressions/SRC/Zbtree.v
ch2_types_expressions/SRC/bin_nums.v
ch2_types_expressions/SRC/sol1.v
ch1_overview/SRC/chap1.v
ch4_dependent_product/SRC/polyminimal.v
ch4_dependent_product/SRC/polymorph.v
ch4_dependent_product/SRC/chap4.v
ch4_dependent_product/SRC/all_perm.v
ch4_dependent_product/SRC/thrice.v
ch6_inductive_data/SRC/height.v
ch6_inductive_data/SRC/value_present.v
ch6_inductive_data/SRC/iota.v
ch6_inductive_data/SRC/chap6.v
ch6_inductive_data/SRC/power_log.v
ch6_inductive_data/SRC/sum.v
ch6_inductive_data/SRC/fzero_present.v
ch6_inductive_data/SRC/month.v
ch6_inductive_data/SRC/bool_cases.v
ch6_inductive_data/SRC/pos_div4.v
ch6_inductive_data/SRC/split.v
ch6_inductive_data/SRC/twofirst.v
ch6_inductive_data/SRC/seasons.v
ch6_inductive_data/SRC/Rat_prelude.v
ch6_inductive_data/SRC/Rat.v
ch6_inductive_data/SRC/exo_frac.v
ch6_inductive_data/SRC/rplus.v
ch6_inductive_data/SRC/positive.v
ch6_inductive_data/SRC/mult2.v
ch6_inductive_data/SRC/exo_sum_f.v
ch6_inductive_data/SRC/emptyset.v
ch6_inductive_data/SRC/depfun.v
ch6_inductive_data/SRC/izero_present.v
ch6_inductive_data/SRC/recursor_for_vectors.v
ch6_inductive_data/SRC/binary_word.v
ch6_inductive_data/SRC/nth_length.v
ch6_inductive_data/SRC/bool_discr.v
ch6_inductive_data/SRC/erato.v
ch6_inductive_data/SRC/lt_3.v
ch6_inductive_data/SRC/more_seasons.v
ch6_inductive_data/SRC/pos_even_bool.v
ch6_inductive_data/SRC/is_January.v
ch6_inductive_data/SRC/nbseats.v
ch6_inductive_data/SRC/poly_tree.v
ch6_inductive_data/SRC/binary_word_or.v
ch6_inductive_data/SRC/tree_bij.v
ch6_inductive_data/SRC/vectorsbis.v
ch6_inductive_data/SRC/two_power.v
ch6_inductive_data/SRC/man_inj.v
ch6_inductive_data/SRC/propositional.v
ch6_inductive_data/SRC/plus_n_O.v
ch6_inductive_data/SRC/first_in_list.v
ch6_inductive_data/SRC/manhattan.v
ch6_inductive_data/SRC/vectors.v
ch6_inductive_data/SRC/partialfunc.v
ch6_inductive_data/SRC/exobool.v
ch12_modules/SRC/DecOrders.v
ch12_modules/SRC/chap12.v
ch12_modules/SRC/list_order.v
ch13_co_inductive_types/SRC/building.v
ch13_co_inductive_types/SRC/finite_or_infinite.v
ch13_co_inductive_types/SRC/bug_infinite.v
ch13_co_inductive_types/SRC/list_inject.v
ch13_co_inductive_types/SRC/Llist_to_list.v
ch13_co_inductive_types/SRC/Tree_Inf.v
ch13_co_inductive_types/SRC/LMap.v
ch13_co_inductive_types/SRC/infinite_impred_prelude.v
ch13_co_inductive_types/SRC/chap13.v
ch13_co_inductive_types/SRC/finiteness_needed.v
ch13_co_inductive_types/SRC/graft.v
ch13_co_inductive_types/SRC/infinite_impred.v
ch13_co_inductive_types/SRC/LTree_bisimilar.v
ch13_co_inductive_types/SRC/graft_absorb.v
ch13_co_inductive_types/SRC/DamienPous_alt.v
ch13_co_inductive_types/SRC/Ltree.v
ch7_tactics_automation/SRC/primes_hyps.v
ch7_tactics_automation/SRC/Zpos_x_tac.v
ch7_tactics_automation/SRC/chap7.v
ch7_tactics_automation/SRC/le_lt_S_eq.v
ch16_proof_by_reflection/SRC/prime_sqrt.v
ch16_proof_by_reflection/SRC/neutral.v
ch16_proof_by_reflection/SRC/chap16.v
ch16_proof_by_reflection/SRC/verif_divide.v
ch8_inductive_predicates/SRC/chap8.v
ch8_inductive_predicates/SRC/parsing.v
ch8_inductive_predicates/SRC/Hoare_sequence.v
ch8_inductive_predicates/SRC/weird_induc2.v
ch8_inductive_predicates/SRC/impredicative.v
ch8_inductive_predicates/SRC/le_diff.v
ch8_inductive_predicates/SRC/JMeqSolution.v
ch8_inductive_predicates/SRC/non_inductive_sorted.v
ch8_inductive_predicates/SRC/JM_assoc.v
ch8_inductive_predicates/SRC/le_prime.v
ch8_inductive_predicates/SRC/le_impred.v
ch8_inductive_predicates/SRC/frobenius.v
ch8_inductive_predicates/SRC/even.v
ch8_inductive_predicates/SRC/infinite_loop.v
ch8_inductive_predicates/SRC/perms.v
ch8_inductive_predicates/SRC/palindrome.v
ch8_inductive_predicates/SRC/magaud.v
ch8_inductive_predicates/SRC/last.v
ch8_inductive_predicates/SRC/id_solution.v
ch8_inductive_predicates/SRC/lt_le.v
ch8_inductive_predicates/SRC/perms2.v
ch8_inductive_predicates/SRC/weird_induc.v
ch8_inductive_predicates/SRC/Hoare_while_rule_bis.v
more_exercises/texts/classic_well_founded.v
more_exercises/texts/vectors.v
more_exercises/solutions/classic_well_founded.v
more_exercises/solutions/vectors.v