1 |
1 |
2 Hints |
2 Hints |
3 ===== |
3 ===== |
4 |
4 |
5 22-Oct-1993 MMW |
5 22-Oct-1993 MMW |
|
6 20-Nov-1993 MMW |
6 |
7 |
7 Some things notable, but not (yet?) covered by the manual. |
8 Some things notable, but not (yet?) covered by the manual. |
8 |
9 |
9 |
10 |
10 - constants of result type prop should always supply concrete syntax; |
11 - constants of result type prop should always supply concrete syntax |
|
12 (elaborate on this in last sect of 'Defining Logics' (?)); |
11 |
13 |
12 - 'Variable --> Constant' possible during rewriting; |
14 - 'Variable --> Constant' possible during rewriting; |
13 |
15 |
14 - 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)"); |
16 - 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)"); |
15 |
17 |
16 - patterns matching any remaining arguments are not possible (i.e. what would |
18 - patterns matching any remaining arguments are not possible (i.e. what would |
17 be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros |
19 be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros |
18 which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't |
20 which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't |
19 match things like Eps(%x. P, a, b, c); |
21 match things like Eps(%x. P, a, b, c); |
20 |
22 |
21 - alpha: the precise manner in which bounds are renamed for printing; |
23 - alpha: document the precise manner in which bounds are renamed for |
|
24 printing; |
22 |
25 |
23 - parsing: applications like f(x)(y)(z) are not parse-ast-translated into |
26 - parsing: applications like f(x)(y)(z) are not parse-ast-translated into |
24 (f x y z); this may cause some problems, when the notation "f x y z" for |
27 (f x y z); this may cause some problems, when the notation "f x y z" for |
25 applications will be introduced; |
28 applications will be introduced; |
26 |
29 |