Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Coq Other
Branch: master

This branch is 20 commits behind math-classes:master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
doc
papers
src
talks/coqworkshop2010
tools
.gitignore
LICENSE
README

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.
Something went wrong with that request. Please try again.