package info (click to toggle)
coq 8.0pl3-2
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 14,376 kB
  • ctags: 17,713
  • sloc: ml: 97,274; makefile: 1,257; sh: 1,215; lisp: 456; awk: 15

Folder: Reals

d .. (parent)
- - rw-r--r-- 25,974 Alembert.v
- - rw-r--r-- 15,715 AltSeries.v
- - rw-r--r-- 6,372 ArithProp.v
- - rw-r--r-- 7,368 Binomial.v
- - rw-r--r-- 14,162 Cauchy_prod.v
- - rw-r--r-- 32,956 Cos_plus.v
- - rw-r--r-- 14,079 Cos_rel.v
- - rw-r--r-- 2,784 DiscrR.v
- - rw-r--r-- 30,243 Exp_prop.v
- - rw-r--r-- 682 Integration.v
- - rw-r--r-- 23,246 MVT.v
- - rw-r--r-- 27,097 NewtonInt.v
- - rw-r--r-- 8,653 PSeries_reg.v
- - rw-r--r-- 18,401 PartSum.v
- - rw-r--r-- 45,888 RIneq.v
- - rw-r--r-- 22,699 RList.v
- - rw-r--r-- 27,097 R_Ifp.v
- - rw-r--r-- 10,916 R_sqr.v
- - rw-r--r-- 13,209 R_sqrt.v
- - rw-r--r-- 23,767 Ranalysis.v
- - rw-r--r-- 46,440 Ranalysis1.v
- - rw-r--r-- 16,094 Ranalysis2.v
- - rw-r--r-- 27,830 Ranalysis3.v
- - rw-r--r-- 11,794 Ranalysis4.v
- - rw-r--r-- 5,787 Raxioms.v
- - rw-r--r-- 691 Rbase.v
- - rw-r--r-- 17,557 Rbasic_fun.v
- - rw-r--r-- 6,513 Rcomplete.v
- - rw-r--r-- 2,197 Rdefinitions.v
- - rw-r--r-- 20,837 Rderiv.v
- - rw-r--r-- 1,468 Reals.v
- - rw-r--r-- 25,169 Rfunctions.v
- - rw-r--r-- 6,612 Rgeom.v
- - rw-r--r-- 124,976 RiemannInt.v
- - rw-r--r-- 99,802 RiemannInt_SF.v
- - rw-r--r-- 21,287 Rlimit.v
- - rw-r--r-- 22,460 Rpower.v
- - rw-r--r-- 6,800 Rprod.v
- - rw-r--r-- 9,854 Rseries.v
- - rw-r--r-- 5,233 Rsigma.v
- - rw-r--r-- 19,790 Rsqrt_def.v
- - rw-r--r-- 8,670 Rsyntax.v
- - rw-r--r-- 67,466 Rtopology.v
- - rw-r--r-- 57,532 Rtrigo.v
- - rw-r--r-- 18,329 Rtrigo_alt.v
- - rw-r--r-- 13,884 Rtrigo_calc.v
- - rw-r--r-- 14,887 Rtrigo_def.v
- - rw-r--r-- 5,542 Rtrigo_fun.v
- - rw-r--r-- 21,505 Rtrigo_reg.v
- - rw-r--r-- 39,610 SeqProp.v
- - rw-r--r-- 14,551 SeqSeries.v
- - rw-r--r-- 986 SplitAbsolu.v
- - rw-r--r-- 834 SplitRmult.v
- - rw-r--r-- 12,075 Sqrt_reg.v