GitHub - roglo/coq_real: Real Numbers using LPO

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 10,599 Commits
poemes		poemes
.depend		.depend
.gitignore		.gitignore
Archimedean.v		Archimedean.v
GQ.v		GQ.v
Makefile		Makefile
Misc.v		Misc.v
Nat_diff.v		Nat_diff.v
Nat_ggcd.v		Nat_ggcd.v
PQ.v		PQ.v
README		README
Rational.v		Rational.v
Small.v		Small.v
Summation.v		Summation.v
Ureal.v		Ureal.v
UrealAddAssoc.v		UrealAddAssoc.v
UrealAddAssoc1.v		UrealAddAssoc1.v
UrealNorm.v		UrealNorm.v
Xnat.v		Xnat.v
bezout.ml		bezout.ml
cat.v		cat.v
def-nb-use.sh		def-nb-use.sh
fourmi.ml		fourmi.ml
fracreal.ml		fracreal.ml
hott.v		hott.v
interface.sh		interface.sh
ocaml.ml		ocaml.ml
prime.ml		prime.ml
select-def.sh		select-def.sh
snake.v		snake.v
zf.v		zf.v

Repository files navigation

Real Numbers implemented using LPO as unique axiom.
Work in progress...

Started on Coq version 8.6.1.
Now using Coq version 8.10 (master version).

The directory "poemes" contains poems written in French (alexandrines)
about this work.