A library of abstract interfaces for mathematical structures in Coq.
Coq Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
categories
functors patch by Jason for case sensitive file systems May 8, 2015
implementations
interfaces
misc Remove wrong instance Oct 29, 2016
orders
quote Change Implicit Arguments to Arguments Feb 23, 2018
site_scons/site_tools merged Coq team's fixes to mathclasses, from branch v8.5 at Mar 1, 2016
theory
varieties Remove deprecated option `Set Automatic Coercions Import`. Jul 20, 2018
.gitignore
.travis.yml
LICENSE
Makefile
README.md Update README.md Jul 20, 2018
SConscript merged Coq team's fixes to mathclasses, from branch v8.5 at Mar 1, 2016
SConstruct merged Coq team's fixes to mathclasses, from branch v8.5 at Mar 1, 2016
_CoqProject.in
configure.sh Rename Make into _CoqProject because of better IDE support. Jul 26, 2018
opam Add OPAM file Jul 16, 2018

README.md

Compilation

This code should compile with 8.6 and later versions. The other branches are deprecated. The code depends on BigNums which can be installed using opam.

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.