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

Authors

Maintainers

Sources

1.3.tar.gz
sha256=12bb7be14e6279d5b3f71427f34ddf777eb63355b0b32282ffe427af3e41e6d9

Description

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

Dependencies (2)

  1. coq-kruskal-trees >= "1.3"
  2. coq >= "8.14" & < "8.20~"

Dev Dependencies

None

Conflicts

None