package coq-fourcolor-reals

  1. Overview
  2. Homepage
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.

Dependencies (1)

  1. coq-mathcomp-algebra

Dev Dependencies (2)

  1. coq-mathcomp-ssreflect (>= "2.1.0" & < "2.5~") | (= "dev")
  2. coq (>= "8.18" & < "9.1~") | (= "dev")

Used by (2)

  1. coq-fourcolor >= "1.4.1"
  2. coq-hol-light >= "2.0.0"

Conflicts (1)

  1. coq-fourcolor != version
Rocq

Interactive Theorem Prover