package coq-kruskal-almostfull
Base Coq library for manipulating Almost Full relations
Install
Dune Dependency
Authors
Maintainers
Sources
Kruskal-AlmostFull-2.0.tar.gz
sha256=72f168db1e7ff342f1c3d8350b2a3f21cfd7faae552ff1e81d71038ce6c55163
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:2025-11-20 logpath:KruskalAfProp logpath:KruskalAfTypePublished: 24 Nov 2025
Dependencies (4)
-
coq-kruskal-finite
>= "2.0" -
coq-kruskal-trees
>= "2.0" - rocq-stdlib
-
rocq-core
>= "9.0.0" & < "9.2~"
Dev Dependencies
None
Used by (5)
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page