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.1.tar.gz
sha256=304a9c8017dd4f1fb4625546a7087172812bce880be723456579d4b0fa92ae22
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-01-19 logpath:KruskalFinitePublished: 19 Jan 2024
Dependencies (3)
-
coq-kruskal-trees
= "1.1" -
coq
>= "8.14" & < "8.19~" - ocaml
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