Skip to content
This repository


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: fd9502ad4f
Fetching contributors…

Cannot retrieve contributors at this time

file 36 lines (30 sloc) 1.321 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36

  Known to compile with Coq trunk 13689.

  Warning: This development assumes a case sensitive file system.

Directory structure:

    Definitions of abstract interfaces/structures.
    Definitions of concrete data structures and algorithms, and proofs
    that they are instances of certain structures (i.e. implement certain interfaces).
    Definitions and theory about orders on different structures.
    Proofs that certain structures form categories.
    Proofs that certain structures are varieties, and translation to/from type classes dedicated
    to these structures (defined in interfaces/).
    Proofs of properties of structures.
    Miscellaneous things.
    Things that currently do not compile.
    Prototype implementation of type class based quoting. To be integrated.
    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.
Something went wrong with that request. Please try again.