README

Compilation

  Known to compile with Coq 8.4 beta

  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.