aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ClassicalConstructiveReals.v
AgeCommit message (Expand)Author
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ...Vincent Semeria