package coq-kruskal-veldman
Wim Veldman's proof of Higman's and Kruskal tree theorems
Install
Dune Dependency
Authors
Maintainers
Sources
Kruskal-Veldman-2.0.tar.gz
sha256=b11c8c25aab91b1561a726031a4dedbf6dd81f6c083d374d92e7cb971c5ab54d
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.
Tags
category:Computer Science/Data Types and Data Structures date:2025-12-11 logpath:KruskalVeldmanProp logpath:KruskalVeldmanTypePublished: 08 Jan 2026
Dependencies (5)
Dev Dependencies
None
Used by (1)
Conflicts
None
On This Page