package coq-kruskal-finite

  1. Overview
  2. Homepage
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.1.1.tar.gz
sha256=c8ca0a1887be7082ecfd39af592dd9ae6077292cf3884c616ab426b12f9b8218

Description

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

Dependencies (3)

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

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover