package info (click to toggle)
rocq-stdlib 9.0.0-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 11,828 kB
  • sloc: python: 2,928; sh: 444; makefile: 319; javascript: 24; ml: 2

Folder: Reals

d .. (parent)
d d rwxr-xr-x 4,096 Abstract
d d rwxr-xr-x 4,096 Cauchy
- - rw-r--r-- 24,783 Alembert.v
- - rw-r--r-- 15,413 AltSeries.v
- - rw-r--r-- 6,744 ArithProp.v
- - rw-r--r-- 8,466 Binomial.v
- - rw-r--r-- 9,140 Cauchy_prod.v
- - rw-r--r-- 12,109 ClassicalConstructiveReals.v
- - rw-r--r-- 27,132 ClassicalDedekindReals.v
- - rw-r--r-- 24,376 Cos_plus.v
- - rw-r--r-- 10,383 Cos_rel.v
- - rw-r--r-- 2,233 DiscrR.v
- - rw-r--r-- 27,858 Exp_prop.v
- - rw-r--r-- 795 Integration.v
- - rw-r--r-- 25,296 MVT.v
- - rw-r--r-- 6,905 Machin.v
- - rw-r--r-- 29,668 NewtonInt.v
- - rw-r--r-- 2,753 Nsatz.v
- - rw-r--r-- 25,702 PSeries_reg.v
- - rw-r--r-- 22,707 PartSum.v
- - rw-r--r-- 5,918 Qreals.v
- - rw-r--r-- 94,634 RIneq.v
- - rw-r--r-- 27,771 RList.v
- - rw-r--r-- 2,918 ROrderedType.v
- - rw-r--r-- 17,608 R_Ifp.v
- - rw-r--r-- 11,894 R_sqr.v
- - rw-r--r-- 14,243 R_sqrt.v
- - rw-r--r-- 1,425 Ranalysis.v
- - rw-r--r-- 63,676 Ranalysis1.v
- - rw-r--r-- 14,840 Ranalysis2.v
- - rw-r--r-- 28,797 Ranalysis3.v
- - rw-r--r-- 13,334 Ranalysis4.v
- - rw-r--r-- 61,152 Ranalysis5.v
- - rw-r--r-- 30,481 Ranalysis_reg.v
- - rw-r--r-- 74,367 Ratan.v
- - rw-r--r-- 17,143 Raxioms.v
- - rw-r--r-- 822 Rbase.v
- - rw-r--r-- 22,325 Rbasic_fun.v
- - rw-r--r-- 8,593 Rcomplete.v
- - rw-r--r-- 12,602 Rdefinitions.v
- - rw-r--r-- 20,326 Rderiv.v
- - rw-r--r-- 1,693 Reals.v
- - rw-r--r-- 29,198 Rfunctions.v
- - rw-r--r-- 7,987 Rgeom.v
- - rw-r--r-- 141,291 RiemannInt.v
- - rw-r--r-- 108,954 RiemannInt_SF.v
- - rw-r--r-- 20,996 Rlimit.v
- - rw-r--r-- 6,443 Rlogic.v
- - rw-r--r-- 3,862 Rminmax.v
- - rw-r--r-- 818 Rpow_def.v
- - rw-r--r-- 30,072 Rpower.v
- - rw-r--r-- 7,259 Rprod.v
- - rw-r--r-- 1,476 Rregisternames.v
- - rw-r--r-- 14,553 Rseries.v
- - rw-r--r-- 5,683 Rsigma.v
- - rw-r--r-- 23,370 Rsqrt_def.v
- - rw-r--r-- 88,504 Rtopology.v
- - rw-r--r-- 1,307 Rtrigo.v
- - rw-r--r-- 64,247 Rtrigo1.v
- - rw-r--r-- 13,308 Rtrigo_alt.v
- - rw-r--r-- 11,406 Rtrigo_calc.v
- - rw-r--r-- 11,914 Rtrigo_def.v
- - rw-r--r-- 6,813 Rtrigo_facts.v
- - rw-r--r-- 5,863 Rtrigo_fun.v
- - rw-r--r-- 15,576 Rtrigo_reg.v
- - rw-r--r-- 20,160 Runcountable.v
- - rw-r--r-- 43,127 SeqProp.v
- - rw-r--r-- 17,273 SeqSeries.v
- - rw-r--r-- 1,073 SplitAbsolu.v
- - rw-r--r-- 959 SplitRmult.v
- - rw-r--r-- 12,354 Sqrt_reg.v
- - rw-r--r-- 4,185 Zfloor.v