aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ConstructiveRealsMorphisms.v
AgeCommit message (Expand)Author
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria