-
Notifications
You must be signed in to change notification settings - Fork 65
Expand file tree
/
Copy path_CoqProject
More file actions
152 lines (135 loc) · 4.81 KB
/
_CoqProject
File metadata and controls
152 lines (135 loc) · 4.81 KB
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
-Q classical mathcomp.classical
-Q reals mathcomp.reals
-Q reals_stdlib mathcomp.reals_stdlib
-Q experimental_reals mathcomp.experimental_reals
-Q theories mathcomp.analysis
-Q analysis_stdlib mathcomp.analysis_stdlib
-arg -w -arg -parsing
-arg -w -arg +undeclared-scope
-arg -w -arg +non-primitive-record
-arg -w -arg -ambiguous-paths
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
classical/all_classical.v
classical/internal_Eqdep_dec.v
classical/all_ssreflect_compat.v
classical/boolp.v
classical/contra.v
classical/wochoice.v
classical/classical_sets.v
classical/mathcomp_extra.v
classical/unstable.v
classical/functions.v
classical/cardinality.v
classical/fsbigop.v
classical/set_interval.v
classical/classical_orders.v
classical/filter.v
reals/constructive_ereal.v
reals/reals.v
reals/real_interval.v
reals/signed.v
reals/prodnormedzmodule.v
reals/all_reals.v
experimental_reals/xfinmap.v
experimental_reals/discrete.v
experimental_reals/realseq.v
experimental_reals/realsum.v
experimental_reals/distr.v
reals_stdlib/Rstruct.v
reals_stdlib/nsatz_realtype.v
theories/ereal.v
theories/landau.v
theories/topology_theory/topology.v
theories/topology_theory/bool_topology.v
theories/topology_theory/compact.v
theories/topology_theory/connected.v
theories/topology_theory/matrix_topology.v
theories/topology_theory/nat_topology.v
theories/topology_theory/order_topology.v
theories/topology_theory/product_topology.v
theories/topology_theory/pseudometric_structure.v
theories/topology_theory/subspace_topology.v
theories/topology_theory/subtype_topology.v
theories/topology_theory/supremum_topology.v
theories/topology_theory/topology_structure.v
theories/topology_theory/uniform_structure.v
theories/topology_theory/weak_topology.v
theories/topology_theory/initial_topology.v
theories/topology_theory/num_topology.v
theories/topology_theory/quotient_topology.v
theories/topology_theory/one_point_compactification.v
theories/topology_theory/sigT_topology.v
theories/topology_theory/discrete_topology.v
theories/topology_theory/separation_axioms.v
theories/topology_theory/metric_structure.v
theories/homotopy_theory/homotopy.v
theories/homotopy_theory/wedge_sigT.v
theories/homotopy_theory/continuous_path.v
theories/ess_sup_inf.v
theories/function_spaces.v
theories/cantor.v
theories/tvs.v
theories/normedtype_theory/num_normedtype.v
theories/normedtype_theory/matrix_normedtype.v
theories/normedtype_theory/ereal_normedtype.v
theories/normedtype_theory/pseudometric_normed_Zmodule.v
theories/normedtype_theory/normed_module.v
theories/normedtype_theory/complete_normed_module.v
theories/normedtype_theory/urysohn.v
theories/normedtype_theory/vitali_lemma.v
theories/normedtype_theory/normedtype.v
theories/sequences.v
theories/realfun.v
theories/exp.v
theories/trigo.v
theories/esum.v
theories/derive.v
theories/numfun.v
theories/measure_theory/measurable_structure.v
theories/measure_theory/measure_function.v
theories/measure_theory/counting_measure.v
theories/measure_theory/dirac_measure.v
theories/measure_theory/probability_measure.v
theories/measure_theory/measure_negligible.v
theories/measure_theory/measure_extension.v
theories/measure_theory/measurable_function.v
theories/measure_theory/measure.v
theories/measurable_realfun.v
theories/lebesgue_stieltjes_measure.v
theories/lebesgue_measure.v
theories/borel_hierarchy.v
theories/lebesgue_integral_theory/simple_functions.v
theories/lebesgue_integral_theory/lebesgue_integral_definition.v
theories/lebesgue_integral_theory/measurable_fun_approximation.v
theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
theories/lebesgue_integral_theory/lebesgue_integrable.v
theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
theories/lebesgue_integral_theory/lebesgue_integral_under.v
theories/lebesgue_integral_theory/lebesgue_Rintegral.v
theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
theories/lebesgue_integral_theory/lebesgue_integral.v
theories/lebesgue_integral_theory/giry.v
theories/ftc.v
theories/hoelder.v
theories/probability_theory/random_variable.v
theories/probability_theory/bernoulli_distribution.v
theories/probability_theory/binomial_distribution.v
theories/probability_theory/uniform_distribution.v
theories/probability_theory/normal_distribution.v
theories/probability_theory/exponential_distribution.v
theories/probability_theory/poisson_distribution.v
theories/probability_theory/beta_distribution.v
theories/probability_theory/probability.v
theories/convex.v
theories/charge.v
theories/kernel.v
theories/pi_irrational.v
theories/gauss_integral.v
theories/all_analysis.v
theories/showcase/summability.v
theories/showcase/pnt.v
analysis_stdlib/Rstruct_topology.v
analysis_stdlib/showcase/uniform_bigO.v