author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 14 Dec 2009 13:59:08 +0100 | |
changeset 749 | df962ca75ffa |
parent 748 | 7e19c4b3ab0f (current diff) |
parent 747 | 76e34dd930f6 (diff) |
child 750 | fe2529a9f250 |
--- a/FIXME-TODO Mon Dec 14 13:58:51 2009 +0100 +++ b/FIXME-TODO Mon Dec 14 13:59:08 2009 +0100 @@ -43,3 +43,7 @@ - We shouldn't use the command 'quotient' as this shadows Larry's quotient. Call it 'quotient_type' + +- Maybe quotient and equiv theorems like the ones for + [QuotList, QuotOption, QuotPair...] could be automatically + proven?