package coq-kruskal-trees

  1. Overview
  2. No Docs
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

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

Maintainers

  1. D
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
  2. J
    Jerome Hugues (https://github.com/jjhugues)

Sources

Kruskal-Trees-1.5.tar.gz
sha256=05029d6575766841a9c036192520471066ec9de04a022a1777fd6b78afd19b04

Description

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

Tags

category:Computer Science/Data Types and Data Structures date:2024-11-21 logpath:KruskalTrees

Published: 22 Nov 2024

Dependencies (1)

  1. coq >= "8.14" & < "8.21~"

Dev Dependencies

None

Conflicts

None