package coq-fourcolor-reals
Interface for real numbers used in the Four Color Theorem
Install
Dune Dependency
Authors
Maintainers
Sources
v1.4.1.tar.gz
sha512=0efc2465fb34bc7013114e835a58efc3649b84924af72dde5e15084532c48f1b17d0582c48f3cf42eec1dc26ca05df7d53958a65fc9b80fa4bfae9e45907397c
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: 21 Apr 2025
Dependencies (1)
Dev Dependencies (2)
-
coq-mathcomp-ssreflect
(>= "2.1.0" & < "2.5~") | (= "dev") -
coq
(>= "8.18" & < "9.1~") | (= "dev")
Used by (4)
-
coq-fourcolor
>= "1.4.1" -
coq-hol-light
>= "2.0.0" - rocq-hollight-logic
- rocq-hollight-logic-unif
Conflicts (1)
-
coq-fourcolor
!= version