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.1.tar.gz
sha256=c8ca0a1887be7082ecfd39af592dd9ae6077292cf3884c616ab426b12f9b8218
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-08 logpath:KruskalFinitePublished: 08 Feb 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