|
103
|
1 |
|
|
|
2 |
Hints
|
|
|
3 |
=====
|
|
|
4 |
|
|
107
|
5 |
22-Oct-1993 MMW
|
|
|
6 |
|
|
|
7 |
Some things notable, but not (yet?) covered by the manual.
|
|
103
|
8 |
|
|
|
9 |
|
|
107
|
10 |
- constants of result type prop should always supply concrete syntax;
|
|
103
|
11 |
|
|
107
|
12 |
- 'Variable --> Constant' possible during rewriting;
|
|
103
|
13 |
|
|
107
|
14 |
- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)");
|
|
103
|
15 |
|
|
107
|
16 |
- 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
|
|
|
18 |
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);
|
|
103
|
20 |
|
|
107
|
21 |
- alpha: the precise manner in which bounds are renamed for printing;
|
|
103
|
22 |
|
|
107
|
23 |
- 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
|
|
|
25 |
applications will be introduced;
|
|
103
|
26 |
|