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.0.tar.gz
md5=f796c38e7135572042830784d99cfcfc
sha512=10a0935933e68795966136c265c7929e3359e640c2eef7562b4d2fe688356ac8ff97da0a75e178b442b7507fb0d37640f8faf700d02c851c6f9905c79c471523
Description
Several implementations for roses trees are proposed with proper induction principles. Sons of the root are collected into dependent vectors, vectors, lists, etc.
Published: 09 Nov 2022
Dev Dependencies
None
Used by (4)
- coq-karp-miller
-
coq-kruskal-higman
>= "1.3" -
coq-kruskal-theorems
>= "1.2" - coq-kruskal-veldman
Conflicts
None
On This Page