changeset 753 | 544b05e03ec0 |
parent 746 | 5ef8be0175f6 |
child 760 | c1989de100b4 |
752:17d06b5ec197 | 753:544b05e03ec0 |
---|---|
45 Call it 'quotient_type' |
45 Call it 'quotient_type' |
46 |
46 |
47 - Maybe quotient and equiv theorems like the ones for |
47 - Maybe quotient and equiv theorems like the ones for |
48 [QuotList, QuotOption, QuotPair...] could be automatically |
48 [QuotList, QuotOption, QuotPair...] could be automatically |
49 proven? |
49 proven? |
50 |
|
51 - Examples: Finite multiset. |