package coq-kruskal-fan
Extending Coq library for manipulating Almost Full relations with the FAN theorem
Install
Dune Dependency
Authors
Maintainers
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:KruskalFanTypePublished: 23 Nov 2024
Dependencies (3)
-
coq-kruskal-almostfull
>= "1.1" -
coq-kruskal-finite
>= "1.4" -
coq-kruskal-trees
>= "1.4"
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