package coq-kruskal-veldman

You can search for identifiers within the package.

in-package search v0.2.0

Wim Veldman's proof of Higman's and Kruskal tree theorems

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

D

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

Maintainers

D

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

Sources

Kruskal-Veldman-2.1.tar.gz

sha256=8b86db55b141125027477902c5c6fc13b27f3c2d98867c9599951f9065f5192c

Description

This library formalizes additional tools for AF relations, eg AF lexicographic induction and relational quasi morphisms applied to Wim Veldman's constructive proof of the tree theorem.

Published: 06 Mar 2026

Dependencies (5)

coq-kruskal-higman >= "2.0"
coq-kruskal-fan >= "2.0"
coq-kruskal-almostfull >= "2.1"
coq-kruskal-finite >= "2.0"
coq-kruskal-trees >= "2.0"

Dev Dependencies

None

Used by (1)

coq-kruskal-theorems

Conflicts