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.2.tar.gz
sha256=0ee07853577a347bc8043ca667f30be79c60573bc2ebb8345d6ed08a525880ea
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-16 logpath:KruskalFinitePublished: 17 Feb 2024
Dependencies (2)
-
coq-kruskal-trees
>= "1.1" -
coq
>= "8.14" & < "8.20~"
Dev Dependencies
None
Used by (4)
- coq-karp-miller
-
coq-kruskal-almostfull
< "1.1" -
coq-kruskal-higman
>= "1.3" - coq-kruskal-veldman
Conflicts
None
On This Page