MathClasses
math-classes is a library of abstract interfaces for mathematical structures.
- Algebraic hierarchy (groups, rings, fields, ...)
- Relations, orders, ...
- Categories, functors, universal algebra, ...
- Numbers: NN, ZZ, QQ, ...
- Operations, ...
It's heavily based on Coq's Type Classes in order to achieve:
- elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory);
- a very flexible purely predicate-based representation of algebraic structures that makes sharing, multiple inheritance, and derived inheritance, all trivial;
- clean expression terms that neither refer to proofs nor require deeply nested record projections;
- fluent rewriting;
- easy and flexible replacement and specialization of data representations and operations with more efficient versions;
- ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.
More information can be found here:
You can find the latest code on github
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.