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