Awesome
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)
What is this library?
This is a collection of tools based on the following notion of finiteness
- a type is finite if it is listable: there is a (computable) list collecting all its members
- a predicate is finite if its span is listable
Dependencies
There is a dependency with Kruskal-Trees
because:
- in the
finite.v
file, we prove finiteness results about the typesidx n
andvec X n
which are actually defined inKruskal-Trees
; - in the
examples/trees.v
, we moreover show that there are finitely many rose trees (ie arbitrarily but finite branching trees) of a given (or bounded) number of nodes, and we needrtree X
andltree X
(and alsolist_sum
).
How to install
This library is CI tested with Coq 8.14
-8.19
and should install smoothly with opam install coq-kruskal-finite
.