package coq-kruskal-veldman

Overview
Homepage

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

Authors

D

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

Maintainers

D

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

Sources

Kruskal-Veldman-2.2.tar.gz

sha256=aa440a136586c5bdf2171e10e9cade2f935a94da916daf030e5cfc6c34446ae2

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

Dependencies (5)

coq-kruskal-higman >= "2.2"
coq-kruskal-fan
coq-kruskal-almostfull >= "2.2"
coq-kruskal-finite
coq-kruskal-trees

Dev Dependencies

None

Used by (1)

coq-kruskal-theorems

Conflicts