diff -r a6f3e1b08494 -r b6873d123f9b Quotient-Paper-jv/TODO --- a/Quotient-Paper-jv/TODO Sat May 12 21:05:59 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -Things to describe not in the original quotient paper: - -* Type maps and Relation maps (show the case for functions) -* Quotient extensions -* Respectfulness and preservation - - Show special cases for quantifiers and lambda -* Quotient-type locale - - Show the proof as much simpler than Homeier's one -* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp) -* Lifting vs Descending vs quot_lifted - - automatic theorem translation heuristic -* Partial equivalence quotients - - Bounded abstraction - - Respects - - partial_descending -* The heuristics for automatic regularization, injection and cleaning. -* A complete example of a lifted theorem together with the regularized - injected and cleaned statement -* Examples of quotients and properties that we used the package for. -* co/contra-variance from Ondrej should be taken into account