		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Def-fgl-rewrite

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

FGL 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 FGL. FGL::DEF-FGL-REWRITE defines a rewrite rule that is only used inside FGL:

(fgl::def-fgl-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 FGL is allowed to use. (FGL will still use it even though it is disabled, as long as it is in that table.)

Def-fgl-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 fgl-object for reference.