package coq-kruskal-trees
Coq library for manipulating rose trees (ie finitely branching) as used in proof of Kruskal's tree theorem
Install
Dune Dependency
Authors
Maintainers
Sources
1.3.tar.gz
sha256=a4086f30d1cffa862c8795f14de9b71969c75559d3157beed8c7025388dfc86e
Description
Several implementations for roses trees are proposed with proper induction principles. Sons of the root are collected into dependent vectors, vectors, lists, etc.
Tags
category:Computer Science/Data Types and Data Structures date:2024-02-16 logpath:KruskalTreesPublished: 28 Feb 2024
Dependencies (1)
-
coq
>= "8.14" & < "8.20~"
Dev Dependencies
None
Used by (7)
- coq-karp-miller
-
coq-kruskal-almostfull
< "1.1"
-
coq-kruskal-fan
< "1.1"
-
coq-kruskal-finite
>= "1.2" & < "1.4"
-
coq-kruskal-higman
!= "1.2"
-
coq-kruskal-theorems
>= "1.2"
- coq-kruskal-veldman
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page