Add-fgl-brewrites
Enable some binder rewrite rules for use in FGL
Adds the given binder rewrite rule runes to the
fgl-binder-rules table so that each such rule will be attempted when terms
with its LHS's leading function symbol is encountered. The exact form of the
rule that is used depends on the invocation: if the name given is simply a
symbol, then the formula of that theorem or function name is used. If the name
is instead a :rewrite rune, then the corresponding lemma is used. A
:formula rune (which is not a valid ACL2 rune but is a valid FGL rune) is
treated the same as a bare symbol.
The literal runes stored in the table are slightly different than the ones
accepted as input: a formula rune is stored as (:bformula name) whereas a
rewrite rune is stored as (:brewrite name).
Subtopics
- Add-fgl-brewrite
- Alias for add-fgl-brewrites that just takes one name.
