equal
deleted
inserted
replaced
26 - The user should be able to give quotient_respects and |
26 - The user should be able to give quotient_respects and |
27 preserves theorems in a more natural form. |
27 preserves theorems in a more natural form. |
28 |
28 |
29 Lower Priority |
29 Lower Priority |
30 ============== |
30 ============== |
|
31 |
|
32 - the quot_lifted attribute should rename variables so they do not |
|
33 suggest that they talk about raw terms. |
31 |
34 |
32 - accept partial equivalence relations |
35 - accept partial equivalence relations |
33 |
36 |
34 - think about what happens if things go wrong (like |
37 - think about what happens if things go wrong (like |
35 theorem cannot be lifted) / proper diagnostic |
38 theorem cannot be lifted) / proper diagnostic |