aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ConstructiveRealsLUB.v
AgeCommit message (Expand)Author
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria