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.2.tar.gz
sha256=dfefdb5c52c003494ba52a93bad9cf89321f3e732d77327354cb108a8c749c09
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: 16 Feb 2024
Dependencies (1)
-
coq
>= "8.14" & < "8.20~"
Dev Dependencies
None
Used by (6)
- coq-karp-miller
-
coq-kruskal-almostfull
< "1.1"
-
coq-kruskal-finite
= "1.2"
-
coq-kruskal-higman
>= "1.3"
-
coq-kruskal-theorems
>= "1.2"
- coq-kruskal-veldman
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page