package coq-deriving

  1. Overview
  2. No Docs
Generic instances of MathComp classes

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

  1. A
    Arthur Azevedo de Amorim

Maintainers

  1. A
    Arthur Azevedo de Amorim <arthur.aa@gmail.com>

Sources

v0.2.0.tar.gz
sha512=8d4cbb22f246add31d48553d67aee39d985f6f1b9c6f1b6c885c6972b50aaeb3fc4b48944b643b994550dcc680fd6d9e5644a3441929d9b3c0d7d4933fe05706

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:deriving

Published: 23 Sep 2023

Dependencies (1)

  1. coq-mathcomp-ssreflect >= "2.0" & < "2.3~"

Dev Dependencies (1)

  1. coq (>= "8.17" & < "8.21~") | (= "dev")

Used by (2)

  1. coq-extructures >= "0.4.0"
  2. coq-ssprove

Conflicts

None