A library of abstract interfaces for mathematical structures in Coq.
|doc||missing double quote|
|papers||typo: aspect -> aspects|
|src||Remove duplicate lemma "neq_symm" of "not_symmetry".|
|talks||talks/coqworkshop2010: Minor fixes.|
|tools||Merge branch 'master' of https://github.com/robbertkrebbers/math-classes|
|.gitignore||Shorter, and hopefully, more consistent names. For example: RingPlus …|
|LICENSE||Add papers and talks.|
|README||Fix compilation with Coq 8.4|
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.