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
Kruskal-Finite-2.0.tar.gz
sha256=b59f32ac80750b5056ce74c3959ca1225c0446599323486994de0df9b93fd279
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:2025-11-20 logpath:KruskalFinitePublished: 24 Nov 2025
Dependencies (3)
-
coq-kruskal-trees
>= "2.0" - rocq-stdlib
-
rocq-core
>= "9.0.0" & < "9.2~"
Dev Dependencies
None
Used by (5)
Conflicts
None
On This Page