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