A library of abstract interfaces for mathematical structures in Coq.
Pull request Compare This branch is 67 commits behind math-classes:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
doc
papers
src
talks/coqworkshop2010
tools
.gitignore
LICENSE
README

README

Compilation

  Known to compile with Coq trunk 14722.

  Warning: This development assumes a case sensitive file system.

Directory structure:

  src/interfaces/
    Definitions of abstract interfaces/structures.
  src/implementations/
    Definitions of concrete data structures and algorithms, and proofs
    that they are instances of certain structures (i.e. implement certain interfaces).
  src/orders/
    Theory about orders on different structures.
  src/categories/
    Proofs that certain structures form categories.
  src/varieties/
    Proofs that certain structures are varieties, and translation to/from type classes dedicated
    to these structures (defined in interfaces/).
  src/theory/
    Proofs of properties of structures.
  src/misc/
    Miscellaneous things.
  src/broken/
    Things that currently do not compile.
  src/quote/
    Prototype implementation of type class based quoting. To be integrated.
  tools/
    Scripts and utilities.

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.