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.1.tar.gz
sha256=0f22b9d88925471275e7f741f776121e0e2bbf89b1fd9d2e903563990f990aec

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-08-28 logpath:KruskalFanProp logpath:KruskalFanType

Published: 28 Aug 2024

Dependencies (3)

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

Dev Dependencies

None

Used by (3)

  1. coq-friedman-tree >= "1.1"
  2. coq-kruskal-higman >= "1.1"
  3. coq-kruskal-veldman >= "1.1" & < "1.3"

Conflicts

None