package coq-kruskal-fan

  1. Overview
  2. No Docs
Extending Coq library for manipulating Almost Full relations with the FAN theorem

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. D
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)

Maintainers

  1. D
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)

Sources

Kruskal-Fan-1.2.tar.gz
sha256=dbd107c4afa5b01a94f69b49f6c33dc7249396865bad9bf82367d5ec49d92c09

Description

This library formalizes additional tools for AF relations, the FAN theorem for inductive bars and a constructive variant of König's lemma.

Tags

category:Computer Science/Data Types and Data Structures date:2024-11-22 logpath:KruskalFanProp logpath:KruskalFanType

Published: 23 Nov 2024

Dependencies (3)

  1. coq-kruskal-almostfull >= "1.1"
  2. coq-kruskal-finite >= "1.4"
  3. coq-kruskal-trees >= "1.4"

Dev Dependencies

None

Conflicts

None