package coq-deriving
Generic instances of MathComp classes
Install
Dune Dependency
Authors
Maintainers
Sources
v0.2.3.tar.gz
sha512=17640ba611cea51527493d7f69b83a2a808e770da20f1144546d4de2136122b9c3b5a00549b518702ba236d6e17abfac0577d59d4463fac9e969cdcb202ab9ba
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: 01 May 2026
Dependencies (1)
-
coq-mathcomp-ssreflect
>= "2.0"
Dev Dependencies (1)
-
coq
(>= "8.17" & < "9.2~") | (= "dev")
Used by (2)
-
coq-extructures
>= "0.4.0" - coq-ssprove
Conflicts
None
On This Page