Compilation
Known to compile with Coq trunk 14023.
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.