coq-dictionaries

Dictionaries (with modules). This file contains a specification for dictionaries, and an implementation using binary search trees. Coq's module system, with module types and functors, is heavily used. It can be considered as a certified version of an example proposed by Paulson in Standard ML. A detailed description (in French) can be found in the chapter 11 of The Coq'Art, the book written by Yves Bertot and Pierre Castéran (please follow the link http://coq.inria.fr/doc-eng.html )

opam install coq-dictionaries.8.5.0
homepage
https://github.com/coq-contribs/dictionaries
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/dictionaries/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/dictionaries/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-dictionaries/coq-dictionaries.8.5.0