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.6.0
homepage
https://github.com/coq-contribs/dictionaries
license
LGPL 2.1
bugs tracker
https://github.com/coq-contribs/dictionaries/issues
dependencies
coq (>= 8.6 & < 8.7~)
source
https://github.com/coq-contribs/dictionaries/archive/v8.6.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-dictionaries/coq-dictionaries.8.6.0