summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/MacroHints

author | wenzelm |

Thu, 11 Nov 1993 10:05:17 +0100 | |

changeset 107 | b4a8dabc7313 |

parent 106 | 7a5d207e6151 |

child 137 | ad5414f5540c |

permissions | -rw-r--r-- |

replaced by current version;

Hints ===== 22-Oct-1993 MMW Some things notable, but not (yet?) covered by the manual. - constants of result type prop should always supply concrete syntax; - '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: 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;