package coq-kruskal-finite
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page