Recent Releases of kruskal-trees

kruskal-trees - Kruskal-Trees v1.5

Added some files for archival via Software Heritage.

- Coq
Published by DmxLarchey over 1 year ago

kruskal-trees - Kruskal-Trees v1.4

Split the clean target into clean and mrproper because of issues with opam install on MacOS: the default find command is not the GNU one (thx to @joom).

- Coq
Published by DmxLarchey almost 2 years ago

kruskal-trees - Kruskal-Trees v1.3

New simple results for List.Forall2: Forall2_{nil,cons,snoc}_inv_{l,r}

- Coq
Published by DmxLarchey over 2 years ago

kruskal-trees - Kruskal-Trees v1.2

New license is MPL-2.0 and updated for Coq 8.19.

- Coq
Published by DmxLarchey over 2 years ago

kruskal-trees - Kruskal-Trees v1.1

Some additional features: - shortlex order on undecorated rose trees rtree; - compatibility layer for Arith lemmas using lia; - decidability of equality for decorated rose trees dtree and vtree; - extensional decidability for vectors.

- Coq
Published by DmxLarchey over 2 years ago

kruskal-trees - Kruskal-Trees v1.0

This is the first release of the Kruskal-Trees library.

- Coq
Published by DmxLarchey over 3 years ago