package coq-kruskal-veldman

Overview
No Docs

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

Authors

D

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

Maintainers

D

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

Sources

v1.0.tar.gz

sha256=8652321ae981b825efa513ff80544eac92a4772305f6e9d5c7de76656b0ccc71

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: 15 Mar 2024

Dependencies (5)

coq-kruskal-higman >= "1.0"
coq-kruskal-almostfull
coq-kruskal-finite
coq-kruskal-trees
coq >= "8.14" & < "8.20~"

Dev Dependencies

None

Used by (1)

coq-kruskal-theorems < "1.1"

Conflicts