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.1.tar.gz
sha512=dc59c2b8b5f73d330c44c33719c6951c7bbdbd67c45b216575e728107625d7a3e495e7a3859aa4f23069b831d9d1133e5c9589bd44976d78e75acb2911d908ef

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: 03 Dec 2024

Dependencies (1)

  1. coq-mathcomp-ssreflect >= "2.0"

Dev Dependencies (1)

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

Used by (2)

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

Conflicts

None