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.2.tar.gz
sha256=ef215b6dc725f79e6db40a788b61baef69469acb3c4d96dc2a808cbe2d947a9b

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.2.0" & < "9.3~"

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover