Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

Math Classes

Docker CI Contributing Code of Conduct Zulip DOI

Math classes is a library of abstract interfaces for mathematical structures, such as:

It is heavily based on Coq’s new type classes in order to provide: structure inference, multiple inheritance/sharing, convenient algebraic manipulation (e.g. rewriting) and idiomatic use of notations.

Meta

Building and installation instructions

The easiest way to install the latest released version of Math Classes is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-math-classes

To instead build and install manually, do:

git clone https://github.com/coq-community/math-classes.git
cd math-classes
./configure.sh
make   # or make -j <number-of-cores-on-your-machine>
make install

Directory structure

categories/

Proofs that certain structures form categories.

functors/

interfaces/

Definitions of abstract interfaces/structures.

implementations/

Definitions of concrete data structures and algorithms, and proofs that they are instances of certain structures (i.e. implement certain interfaces).

misc/

Miscellaneous things.

orders/

Theory about orders on different structures.

quote/

Prototype implementation of type class based quoting. To be integrated.

theory/

Proofs of properties of structures.

varieties/

Proofs that certain structures are varieties, and translation to/from type classes dedicated to these structures (defined in interfaces/).

The reason we treat categories and varieties differently from other structures (like groups and rings) is that they are like meta-interfaces whose implementations are not concrete data structures and algorithms but are themselves abstract structures.

To be able to distinguish the various arrows, we recommend using a variable width font.