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.v1.0.tar.gz
sha256=33b677dbbde833520744112926fd9e3aa07f220a2c6faa71b51ad92932e8ee06

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-05-21 logpath:KruskalFanProp logpath:KruskalFanType

Published: 23 May 2024

Dependencies (3)

  1. coq-kruskal-almostfull >= "1.0"
  2. coq-kruskal-finite >= "1.3"
  3. coq-kruskal-trees >= "1.3"

Dev Dependencies

None

Used by (3)

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

Conflicts

None