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.1.tar.gz
sha256=c8ca0a1887be7082ecfd39af592dd9ae6077292cf3884c616ab426b12f9b8218

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-02-08 logpath:KruskalFinite

Published: 08 Feb 2024

Dependencies (3)

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

Dev Dependencies

None

Conflicts

None