package coq-kruskal-almostfull

  1. Overview
  2. Homepage
Base Coq library for manipulating Almost Full relations

Install

Dune Dependency

Authors

Maintainers

Sources

Kruskal-AlmostFull-2.1.tar.gz
sha256=ab4a1d26ab41828963cb1d54a627fa389769855d201bf76dca3205c4b47f85d9

Description

This library formalizes ground results about Almost Full relations (AF) in Coq 8.14+, up to Dickson's lemma.

Dependencies (4)

  1. coq-kruskal-finite >= "2.0"
  2. coq-kruskal-trees >= "2.0"
  3. rocq-stdlib
  4. rocq-core >= "9.0.0" & < "9.2~"

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover