Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Failed to load latest commit information.|
Compilation Known to compile with Coq 8.4 which can be obtained from http://pauillac.inria.fr/~herbelin/coq/distrib/V8.4/files/coq-8.4.tar.gz 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.