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.2.tar.gz
sha256=0be35bc4d6d6c5e623b25fbed65b43c1b506615929a2c5400e3be84144f2ab4a
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:2026-04-12 logpath:KruskalFinitePublished: 13 Apr 2026
Dependencies (3)
-
coq-kruskal-trees
>= "2.2" - rocq-stdlib
-
rocq-core
>= "9.2.0" & < "9.3~"
Dev Dependencies
None
Used by (5)
Conflicts
None
On This Page