package coq-kruskal-trees

Overview
Homepage

You can search for identifiers within the package.

in-package search v0.2.0

Coq library for manipulating rose trees (ie finitely branching) as used in proof of Kruskal's tree theorem

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

Jerome Hugues (https://github.com/jjhugues)

Sources

1.3.tar.gz

sha256=a4086f30d1cffa862c8795f14de9b71969c75559d3157beed8c7025388dfc86e

Description

Several implementations for roses trees are proposed with proper induction principles. Sons of the root are collected into dependent vectors, vectors, lists, etc.

Published: 28 Feb 2024

Dependencies (1)

coq >= "8.14" & < "8.20~"

Dev Dependencies

None

Used by (7)

coq-karp-miller
coq-kruskal-almostfull < "1.1"
coq-kruskal-fan < "1.1"
coq-kruskal-finite >= "1.2" & < "1.4"
coq-kruskal-higman != "1.2"
coq-kruskal-theorems >= "1.2"
coq-kruskal-veldman

Conflicts