package coq-fourcolor-reals
Interface for real numbers used in the Four Color Theorem
Install
Dune Dependency
Authors
Maintainers
Sources
v1.4.3.tar.gz
sha512=b92ad5076d72a161e4b95f6264e172efca6154dc6f5ee424244f0c00a1e9e36df30edb868f8080eeffd8f0a8f923383144262f9ce199a626cf0f6bdbc8111399
Description
An axiomatization of the setoid of classical real numbers, along with proofs of properties such as categoricity.
Tags
category:Mathematics/Real Calculus and Topology keyword:real numbers logpath:fourcolor.reals date:2026-07-17Published: 24 Jul 2026
Dependencies (4)
- coq-mathcomp-algebra
-
coq-mathcomp-ssreflect
>= "2.5.0" & < "2.7~" -
rocq-core
>= "9.0" & < "9.4~" -
coq
>= "8.20" & < "8.21~"
Dev Dependencies
None
Used by (3)
-
coq-fourcolor
>= "1.4.3" -
coq-hol-light
>= "2.0.0" - rocq-hollight-logic
Conflicts (1)
-
coq-fourcolor
!= version
On This Page