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 (5)

Authors

D

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

Maintainers

D

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

Sources

Kruskal-Theorems-2.2.tar.gz

sha256=a70c72a3ee91bb307e36bcc65c21fee648e5cace0942f86daa4e7993a933ecf8

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: 13 Apr 2026

Dependencies (4)

Dev Dependencies

None

Used by (1)

coq-friedman-tree

Conflicts