package coq-kruskal-theorems

You can search for identifiers within the package.

in-package search v0.2.0

Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

D

Dominique Larchey-Wendling (https://github.com/DmxLarchey)

Maintainers

D

Dominique Larchey-Wendling (https://github.com/DmxLarchey)

Sources

Kruskal-Theorems-2.0.tar.gz

sha256=5f407ff42211979eaa10a3a2b05e8562954bfb78712844f6d70a85a50923c54d

Description

This library formalizes the high-level variants of Higman's theorem (for trees of bounded arity) and Kruskal's theorem (for rose trees), depending on how these datatypes are implemented. Also, Vazsonyi's conjecture to illustrate the expressive power of Kruskal's and Higman's theorem.

Published: 08 Jan 2026

Dependencies (4)

Dev Dependencies

None

Used by (1)

coq-friedman-tree

Conflicts