package coq-deriving
Generic instances of MathComp classes
Install
Dune Dependency
Authors
Maintainers
Sources
v0.2.2.tar.gz
sha512=f0546acc0134f33ab43340a405bb6ae5936b59d92d38f29ccf4dad04b8328d5e5ce510d1a866afb8547dce969fc715f6584715b6ef905532d3558ca03795ffad
Description
Deriving provides generic instances of MathComp classes for inductive data types. It includes native support for eqType, choiceType, countType and finType instances, and it allows users to define their own instances for other classes.
Tags
keyword:generic programming category:Computer Science/Data Types and Data Structures logpath:derivingPublished: 18 Apr 2025
Dependencies (1)
-
coq-mathcomp-ssreflect
>= "2.0"
Dev Dependencies (1)
-
coq
(>= "8.17" & < "9.1~") | (= "dev")
Used by (2)
-
coq-extructures
>= "0.4.0" - coq-ssprove
Conflicts
None
On This Page