package coq-kruskal-almostfull
Base Coq library for manipulating Almost Full relations
Install
Dune Dependency
Authors
Maintainers
Sources
Kruskal-AlmostFull-2.2.tar.gz
sha256=ef215b6dc725f79e6db40a788b61baef69469acb3c4d96dc2a808cbe2d947a9b
Description
This library formalizes ground results about Almost Full relations (AF) in Coq 8.14+, up to Dickson's lemma.
Tags
category:Computer Science/Data Types and Data Structures date:2026-04-12 logpath:KruskalAfProp logpath:KruskalAfTypePublished: 13 Apr 2026
Dependencies (4)
-
coq-kruskal-finite
>= "2.0" -
coq-kruskal-trees
>= "2.0" - rocq-stdlib
-
rocq-core
>= "9.2.0" & < "9.3~"
Dev Dependencies
None
Used by (5)
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page