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.2.tar.gz
sha256=73f7c247de10f31a2343dd458ac58ecea9d297036fa2273d9372151420cf3b49
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-04-12 logpath:KruskalFanProp logpath:KruskalFanTypePublished: 13 Apr 2026
Dependencies (3)
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