package coq-kruskal-veldman

  1. Overview
  2. No Docs
Wim Veldman's proof of Higman's and Kruskal tree theorems

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

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

Maintainers

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

Sources

Kruskal-Veldman.1.1.tar.gz
sha256=6e7f250d3ca09c23e74d4aaaa1dbc22b60999194b04d67a2759a6b6ab5b44efe

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:2024-05-23 logpath:KruskalVeldmanProp logpath:KruskalVeldmanType

Published: 23 May 2024

Dev Dependencies

None

Used by (1)

  1. coq-kruskal-theorems < "1.1"

Conflicts

None