Containers: a typeclass-based library of finite sets/maps
- Stéphane Lescuyer
This is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. See tests files for usage. A new vernacular command is provided by Generate.v and the plugin to automatically generate ordered types for user-defined inductive types.
data structures, type classes
Containers: a typeclass-based library of finite sets/maps ========================================================= Copyright 2010 Stéphane Lescuyer <email@example.com> Features ======== A reimplementation of the FSets/FMaps library from the standard library, using typeclasses. See tests files for usage. A new vernacular command is provided by Generate.v and the plugin to automatically generate ordered types for user-defined inductive types. Files ===== The archive has 4 subdirectories: src/ contains the code of the plugin and commands theories/ contains all the vernacular files of the library and Generate.v, used to load the [Generate] plugin in Coq tests/ just demonstrates usage of the basic data structures docs/ contains an in-depth description of the Generate OrderedType vernacular, and a guide to start using this library Installation ============ First, you should have coqc, ocamlc and make in your path. Then simply do: # make -j To consecutively build the plugin and the supporting theories. Optionally you can launch the tests and benchmarks with # make test You can then either install the plugin with # sudo make install or leave it in its current directory and to be able to import it from anywhere in Coq, simply add the following to ~/.coqrc: Add Rec LoadPath "path_to_containers/theories" as Containers. Add ML Path "path_to_containers/src".