package coq-kruskal-finite

  1. Overview
  2. No Docs
Coq library for manipulating finiteness, finite choice and decision 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)

Sources

1.1.tar.gz
sha256=304a9c8017dd4f1fb4625546a7087172812bce880be723456579d4b0fa92ae22

Description

Tools to facilitate proofs of finiteness (ie listability), finite choice principles and finite decidability.

Tags

category:Computer Science/Data Types and Data Structures date:2024-01-19 logpath:KruskalFinite

Published: 19 Jan 2024

Dependencies (3)

  1. coq-kruskal-trees = "1.1"
  2. coq >= "8.14" & < "8.19~"
  3. ocaml

Dev Dependencies

None

Conflicts

None