doc-src/MacroHints
author clasohm
Tue, 09 May 1995 10:42:23 +0200
changeset 1112 737a1a0df754
parent 137 ad5414f5540c
permissions -rw-r--r--
added \CHOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     1
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     2
Hints
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     3
=====
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     4
107
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
     5
22-Oct-1993 MMW
137
ad5414f5540c *** empty log message ***
wenzelm
parents: 107
diff changeset
     6
20-Nov-1993 MMW
107
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
     7
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
     8
Some things notable, but not (yet?) covered by the manual.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     9
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    10
137
ad5414f5540c *** empty log message ***
wenzelm
parents: 107
diff changeset
    11
- constants of result type prop should always supply concrete syntax
ad5414f5540c *** empty log message ***
wenzelm
parents: 107
diff changeset
    12
  (elaborate on this in last sect of 'Defining Logics' (?));
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    13
107
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    14
- 'Variable --> Constant' possible during rewriting;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    15
107
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    16
- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)");
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    17
107
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    18
- patterns matching any remaining arguments are not possible (i.e. what would
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    19
  be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    20
  which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    21
  match things like Eps(%x. P, a, b, c);
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    22
137
ad5414f5540c *** empty log message ***
wenzelm
parents: 107
diff changeset
    23
- alpha: document the precise manner in which bounds are renamed for
ad5414f5540c *** empty log message ***
wenzelm
parents: 107
diff changeset
    24
  printing;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    25
107
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    26
- parsing: applications like f(x)(y)(z) are not parse-ast-translated into
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    27
  (f x y z); this may cause some problems, when the notation "f x y z" for
b4a8dabc7313 replaced by current version;
wenzelm
parents: 106
diff changeset
    28
  applications will be introduced;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    29