package info
(click to toggle)
coq 8.0pl2-2
- links: PTS
- area: main
- in suites: sarge
- size: 14,228 kB
- ctags: 17,685
- sloc: ml: 97,070; makefile: 1,255; sh: 738; lisp: 456; awk: 15
Folder: Reals
.. (parent) | ||||
- | rw-r--r-- | 27,392 | Alembert.v | |
- | rw-r--r-- | 15,849 | AltSeries.v | |
- | rw-r--r-- | 6,858 | ArithProp.v | |
- | rw-r--r-- | 7,582 | Binomial.v | |
- | rw-r--r-- | 14,838 | Cauchy_prod.v | |
- | rw-r--r-- | 31,885 | Cos_plus.v | |
- | rw-r--r-- | 13,012 | Cos_rel.v | |
- | rw-r--r-- | 3,044 | DiscrR.v | |
- | rw-r--r-- | 31,422 | Exp_prop.v | |
- | rw-r--r-- | 682 | Integration.v | |
- | rw-r--r-- | 24,548 | MVT.v | |
- | rw-r--r-- | 28,127 | NewtonInt.v | |
- | rw-r--r-- | 9,315 | PSeries_reg.v | |
- | rw-r--r-- | 19,695 | PartSum.v | |
- | rw-r--r-- | 47,499 | RIneq.v | |
- | rw-r--r-- | 26,120 | RList.v | |
- | rw-r--r-- | 25,367 | R_Ifp.v | |
- | rw-r--r-- | 11,302 | R_sqr.v | |
- | rw-r--r-- | 14,377 | R_sqrt.v | |
- | rw-r--r-- | 28,570 | Ranalysis.v | |
- | rw-r--r-- | 49,801 | Ranalysis1.v | |
- | rw-r--r-- | 16,309 | Ranalysis2.v | |
- | rw-r--r-- | 28,782 | Ranalysis3.v | |
- | rw-r--r-- | 12,491 | Ranalysis4.v | |
- | rw-r--r-- | 5,197 | Raxioms.v | |
- | rw-r--r-- | 691 | Rbase.v | |
- | rw-r--r-- | 17,121 | Rbasic_fun.v | |
- | rw-r--r-- | 6,647 | Rcomplete.v | |
- | rw-r--r-- | 2,224 | Rdefinitions.v | |
- | rw-r--r-- | 18,481 | Rderiv.v | |
- | rw-r--r-- | 1,468 | Reals.v | |
- | rw-r--r-- | 24,828 | Rfunctions.v | |
- | rw-r--r-- | 7,564 | Rgeom.v | |
- | rw-r--r-- | 132,321 | RiemannInt.v | |
- | rw-r--r-- | 108,310 | RiemannInt_SF.v | |
- | rw-r--r-- | 19,933 | Rlimit.v | |
- | rw-r--r-- | 22,751 | Rpower.v | |
- | rw-r--r-- | 7,200 | Rprod.v | |
- | rw-r--r-- | 9,363 | Rseries.v | |
- | rw-r--r-- | 5,374 | Rsigma.v | |
- | rw-r--r-- | 21,263 | Rsqrt_def.v | |
- | rw-r--r-- | 73,296 | Rtopology.v | |
- | rw-r--r-- | 61,361 | Rtrigo.v | |
- | rw-r--r-- | 17,946 | Rtrigo_alt.v | |
- | rw-r--r-- | 15,259 | Rtrigo_calc.v | |
- | rw-r--r-- | 14,582 | Rtrigo_def.v | |
- | rw-r--r-- | 5,209 | Rtrigo_fun.v | |
- | rw-r--r-- | 22,210 | Rtrigo_reg.v | |
- | rw-r--r-- | 41,746 | SeqProp.v | |
- | rw-r--r-- | 15,494 | SeqSeries.v | |
- | rw-r--r-- | 977 | SplitAbsolu.v | |
- | rw-r--r-- | 846 | SplitRmult.v | |
- | rw-r--r-- | 12,800 | Sqrt_reg.v | |
- | rw-r--r-- | 122 | intro.tex |