package coq-graph-theory-planar
Graph theory results on planarity in Coq and MathComp
Install
Dune Dependency
Authors
Maintainers
Sources
graph-theory-0.9.6.tar.gz
sha512=61bd37facc9341c45cb8393b6be5885a424208c74c09eb8366fc263bd7f0904bd6b4c5bd419add4fcdc01d244d6a261701ec33469b6e645b54f8a89c95bb5485
Description
Formal definitions and results on graph planarity in Coq using the Mathematical Components library, including Wagner's Theorem. Relies on hypermaps and other notions developed as part of the Coq proof of the Four-Color Theorem.
Tags
category:Computer Science/Graph Theory keyword:graph theory keyword:planarity logpath:GraphTheory.planar date:2024-06-30Published: 10 May 2025
Dependencies (5)
- coq-fourcolor
-
coq-graph-theory
= version -
coq-mathcomp-ssreflect
>= "2.1" & < "2.5~" -
coq
>= "8.18" & < "9.1~" -
dune
>= "3.5"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page