package coq-kruskal-fan
Extending Coq library for manipulating Almost Full relations with the FAN theorem
Install
Dune Dependency
Authors
Maintainers
Sources
Kruskal-Fan-2.1.tar.gz
sha256=76616b5e2cd34ae0303c33123272aa7eae8595f72e66185370118807b879cb67
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:2026-03-02 logpath:KruskalFanProp logpath:KruskalFanTypePublished: 03 Mar 2026
Dependencies (3)
-
coq-kruskal-almostfull
>= "2.0" -
coq-kruskal-finite
>= "2.0" -
coq-kruskal-trees
>= "2.0"
Dev Dependencies
None
Used by (3)
-
coq-friedman-tree
>= "1.1" -
coq-kruskal-higman
>= "1.1" -
coq-kruskal-veldman
>= "1.1"
Conflicts
None
On This Page