| changeset 746 | 5ef8be0175f6 |
| parent 716 | 1e08743b6997 |
| child 753 | 544b05e03ec0 |
| 742:198ff5781844 | 746:5ef8be0175f6 |
|---|---|
41 |
41 |
42 - Check all the places where we do "handle _" |
42 - Check all the places where we do "handle _" |
43 |
43 |
44 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
44 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
45 Call it 'quotient_type' |
45 Call it 'quotient_type' |
46 |
|
47 - Maybe quotient and equiv theorems like the ones for |
|
48 [QuotList, QuotOption, QuotPair...] could be automatically |
|
49 proven? |