package coq-kruskal-finite
Coq library for manipulating finiteness, finite choice and decision as used in proof of Kruskal's tree theorem
Install
Dune Dependency
Authors
Maintainers
Sources
1.3.tar.gz
sha256=12bb7be14e6279d5b3f71427f34ddf777eb63355b0b32282ffe427af3e41e6d9
Description
Tools to facilitate proofs of finiteness (ie listability), finite choice principles and finite decidability.
Tags
category:Computer Science/Data Types and Data Structures date:2024-02-28 logpath:KruskalFinitePublished: 29 Feb 2024
Dependencies (2)
-
coq-kruskal-trees
>= "1.3" -
coq
>= "8.14" & < "8.20~"
Dev Dependencies
None
Used by (5)
- coq-karp-miller
-
coq-kruskal-almostfull
< "1.1" -
coq-kruskal-fan
< "1.1" -
coq-kruskal-higman
!= "1.2" - coq-kruskal-veldman
Conflicts
None
On This Page