Skip to content

index.markdown

Latest commit

 

History

History
39 lines (28 loc) · 1.12 KB

index.markdown

File metadata and controls

39 lines (28 loc) · 1.12 KB
layout default
title About

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

  • Algebraic hierarchy (groups, rings, fields, ...)
  • Relations, orders, ...
  • Categories, functors, universal algebra, ...
  • Numbers: ℕ, ℤ, ℚ, ...
  • Operations, (shift, power, abs, ...)

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

Here is a SVG diagram showing all files and their dependencies with links to the coqdoc dependencies.

Here are two diagrams showing the main components of the algebraic hierarchy and the various orders in math classes.

Algebraic Hierarchy Order Hierarchy

Math classes is used in C-CoRN to implement high performance exact real number arithmetic.

Install

Add the Coq repository:

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

and run:

opam install coq-math-classes