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:2025-04-16Published: 24 Jul 2026
Dependencies (1)
Dev Dependencies (2)
-
coq-mathcomp-ssreflect
(>= "2.4.0" & < "2.6~") | (= "dev") -
coq
(>= "8.20" & < "9.2~") | (= "dev")
Used by (3)
-
coq-fourcolor
>= "1.4.3" -
coq-hol-light
>= "2.0.0" - rocq-hollight-logic
Conflicts (1)
-
coq-fourcolor
!= version