aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ClassicalConstructiveReals.v
AgeCommit message (Collapse)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
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental