package coq-fourcolor-reals
Interface for real numbers used in the Four Color Theorem
Install
Dune Dependency
Authors
Maintainers
Sources
v1.4.2.tar.gz
sha512=67191d0552fac710ba1a06d83df3266dc359a80c8c706b3631d2d6e5a4e99c87011bc65ca1daadfaff0cf5b3c26a6eb808bffb183cc00c41436bd237dbeb1467
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: 13 Nov 2025
Dependencies (1)
Dev Dependencies (2)
-
coq-mathcomp-ssreflect
(>= "2.4.0" & < "2.6~") | (= "dev") -
coq
(>= "8.20" & < "9.2~") | (= "dev")
Used by (4)
-
coq-fourcolor
>= "1.4.2" -
coq-hol-light
>= "2.0.0" - rocq-hollight-logic
- rocq-hollight-logic-unif
Conflicts (1)
-
coq-fourcolor
!= version