| changeset 749 | df962ca75ffa |
| parent 746 | 5ef8be0175f6 |
| child 753 | 544b05e03ec0 |
| 748:7e19c4b3ab0f | 749:df962ca75ffa |
|---|---|
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? |