index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Reals
Mode
Name
Size
-rw-r--r--
Alembert.v
26039
log
plain
-rw-r--r--
AltSeries.v
15735
log
plain
-rw-r--r--
ArithProp.v
6245
log
plain
-rw-r--r--
Binome.v
7239
log
plain
-rw-r--r--
Cauchy_prod.v
14008
log
plain
-rw-r--r--
Cos_plus.v
32766
log
plain
-rw-r--r--
Cos_rel.v
13927
log
plain
-rw-r--r--
DiscrR.v
1808
log
plain
-rw-r--r--
Exp_prop.v
30190
log
plain
-rw-r--r--
Integration.v
616
log
plain
-rw-r--r--
NewtonInt.v
27008
log
plain
-rw-r--r--
PSeries_reg.v
8500
log
plain
-rw-r--r--
PartSum.v
18269
log
plain
-rw-r--r--
RList.v
22815
log
plain
-rw-r--r--
R_Ifp.v
26950
log
plain
-rw-r--r--
R_sqr.v
10807
log
plain
-rw-r--r--
R_sqrt.v
13342
log
plain
-rw-r--r--
Ranalysis.v
23698
log
plain
-rw-r--r--
Ranalysis1.v
45494
log
plain
-rw-r--r--
Ranalysis2.v
16128
log
plain
-rw-r--r--
Ranalysis3.v
27583
log
plain
-rw-r--r--
Ranalysis4.v
11677
log
plain
-rw-r--r--
Raxioms.v
5138
log
plain
-rw-r--r--
Rbase.v
45032
log
plain
-rw-r--r--
Rbasic_fun.v
17409
log
plain
-rw-r--r--
Rcomplet.v
6293
log
plain
-rw-r--r--
Rdefinitions.v
1440
log
plain
-rw-r--r--
Rderiv.v
20725
log
plain
-rw-r--r--
Reals.v
685
log
plain
-rw-r--r--
RealsB.v
658
log
plain
-rw-r--r--
Rfunctions.v
24986
log
plain
-rw-r--r--
Rgeom.v
6502
log
plain
-rw-r--r--
RiemannInt.v
124035
log
plain
-rw-r--r--
RiemannInt_SF.v
99546
log
plain
-rw-r--r--
Rlimit.v
21175
log
plain
-rw-r--r--
Rpower.v
22349
log
plain
-rw-r--r--
Rprod.v
6650
log
plain
-rw-r--r--
Rseries.v
9675
log
plain
-rw-r--r--
Rsigma.v
5085
log
plain
-rw-r--r--
Rsqrt_def.v
19743
log
plain
-rw-r--r--
Rsyntax.v
8313
log
plain
-rw-r--r--
Rtopology.v
68252
log
plain
-rw-r--r--
Rtrigo.v
57556
log
plain
-rw-r--r--
Rtrigo_alt.v
18374
log
plain
-rw-r--r--
Rtrigo_calc.v
14614
log
plain
-rw-r--r--
Rtrigo_def.v
14890
log
plain
-rw-r--r--
Rtrigo_fun.v
5390
log
plain
-rw-r--r--
Rtrigo_reg.v
21319
log
plain
-rw-r--r--
SeqProp.v
41280
log
plain
-rw-r--r--
SeqSeries.v
8418
log
plain
-rw-r--r--
SplitAbsolu.v
900
log
plain
-rw-r--r--
SplitRmult.v
760
log
plain
-rw-r--r--
Sqrt_reg.v
11960
log
plain
-rw-r--r--
TAF.v
23136
log
plain
-rw-r--r--
TypeSyntax.v
1223
log
plain
-rw-r--r--
intro.tex
122
log
plain