|
1 Highest Priority |
|
2 ================ |
|
3 |
|
4 - better lookup mechanism for quotient definition |
|
5 (see fixme in quotient_term.ML) |
|
6 |
|
7 - check needs to be fixed in mk_resp_arg (quotient_term.ML), |
|
8 see test for (_, Const _) |
|
9 |
|
10 - clever code in quotiet_tacs.ML needs to be turned into |
|
11 boring code |
|
12 |
|
13 - comment about regularize tactic eeds to be adapted |
|
14 |
|
15 - Check all the places where we do "handle _" |
|
16 (They make code changes very difficult: I sat 1/2 |
|
17 a day over simplification of calculate_inst before |
|
18 I understood things; the reason was that my exceptions |
|
19 where caught by the catch all. There is no problem |
|
20 with throwing and handling exceptions...it just must |
|
21 be clear who throws what ad what is thrown.) |
|
22 |
1 Higher Priority |
23 Higher Priority |
2 =============== |
24 =============== |
3 |
25 |
4 - if the constant definition gives the wrong definition |
26 - if the constant definition gives the wrong definition |
5 term, one gets a cryptic message about get_fun |
27 term, one gets a cryptic message about absrep_fun |
6 |
28 |
7 - have FSet.thy to have a simple infrastructure for |
29 - have FSet.thy to have a simple infrastructure for |
8 finite sets (syntax should be \<lbrace> \<rbrace>, |
30 finite sets (syntax should be \<lbrace> \<rbrace>, |
9 look at Set.thy how syntax is been introduced) |
31 look at Set.thy how syntax is been introduced) |
10 |
32 |
13 quotienting? |
35 quotienting? |
14 |
36 |
15 - user should be able to give quotient_respects and |
37 - user should be able to give quotient_respects and |
16 preserves theorems in a more natural form. |
38 preserves theorems in a more natural form. |
17 |
39 |
18 - the test in the (_, Const _) needs to be fixed |
40 |
19 |
41 |
20 Lower Priority |
42 Lower Priority |
21 ============== |
43 ============== |
22 |
44 |
23 - Maybe a quotient_definition should already require |
45 - Maybe a quotient_definition should already require |
24 a proof of the respectfulness (in this way one |
46 a proof of the respectfulness (in this way one |
25 already excludes non-sensical definitions) |
47 already excludes non-sensical definitions) |
26 |
48 |
27 - accept partial equvalence relations |
49 - accept partial equivalence relations |
28 |
50 |
29 - think about what happens if things go wrong (like |
51 - think about what happens if things go wrong (like |
30 theorem cannot be lifted) / proper diagnostic |
52 theorem cannot be lifted) / proper diagnostic |
31 messages for the user |
53 messages for the user |
32 |
54 |
43 |
65 |
44 - use lower-case letters where appropriate in order |
66 - use lower-case letters where appropriate in order |
45 to make Markus happy |
67 to make Markus happy |
46 |
68 |
47 - add tests for adding theorems to the various thm lists |
69 - add tests for adding theorems to the various thm lists |
48 |
|
49 |
|
50 - Check all the places where we do "handle _" |
|
51 |
70 |
52 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
71 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
53 Call it 'quotient_type' |
72 Call it 'quotient_type' |
54 |
73 |
55 - Maybe quotient and equiv theorems like the ones for |
74 - Maybe quotient and equiv theorems like the ones for |