		Search-engine friendly clone of the ACL2 documentation.

Def-gl-rewrite

Define a rewrite rule for GL to use on term-level objects

GL can use ACL2-style rewrite rules to simplify term-level symbolic objects. However, typically one wants a different theory for ACL2 theorem proving than one wants to use inside GL. GL::DEF-GL-REWRITE defines a rewrite rule that is only used inside GL:

(gl::def-gl-rewrite my-rewrite-rule
   (implies (and (syntaxp (and (integerp n) (< 0 (integer-length n))))
                 (< 0 m))
            (equal (logand n m)
                   (logcons (b-and (logcar n) (logcar m))
                            (logand (logcdr n) (logcdr m)))))
  :hints ...)

This defines a disabled ACL2 rewrite rule called my-rewrite-rule, and adds my-rewrite-rule to the table of rules GL is allowed to use. (GL will still use it even though it is disabled, as long as it is in that table.)

Def-gl-rewrite supports syntaxp hypotheses, but the term representation used is different from ACL2's. Instead of being bound to TERMPs, the variables are bound to symbolic objects. See symbolic-objects for reference.