summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 02 Dec 1996 10:19:52 +0100 | |

changeset 2285 | b239c202c91f |

parent 2284 | 80ebd1a213fd |

child 2286 | c2f76a5bad65 |

removed;

doc-src/MacroHints | file | annotate | diff | comparison | revisions |

--- a/doc-src/MacroHints Fri Nov 29 18:03:21 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ - -Hints -===== - -22-Oct-1993 MMW -20-Nov-1993 MMW - -Some things notable, but not (yet?) covered by the manual. - - -- constants of result type prop should always supply concrete syntax - (elaborate on this in last sect of 'Defining Logics' (?)); - -- 'Variable --> Constant' possible during rewriting; - -- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)"); - -- patterns matching any remaining arguments are not possible (i.e. what would - be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros - which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't - match things like Eps(%x. P, a, b, c); - -- alpha: document the precise manner in which bounds are renamed for - printing; - -- parsing: applications like f(x)(y)(z) are not parse-ast-translated into - (f x y z); this may cause some problems, when the notation "f x y z" for - applications will be introduced; -