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 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.