package coq-kruskal-trees

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

Install

Dune Dependency

Authors

Maintainers

Sources

1.1.tar.gz
sha256=98d9ea2b7b37a2b42ad3dcab748ff0cfbfdff007a5f6e8409e0e37d1eb38ce19

Description

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

Dependencies (2)

  1. coq >= "8.14" & < "8.19~"
  2. ocaml

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover