ACL2-pc::x
(atomic macro)
expand and (maybe) simplify function call at the current subterm
Examples:
x -- expand and simplify.
Also see ACL2-pc::expand and see ACL2-pc::x-dumb, which do
not perform simplification.
For example, if the current subterm is (append a b), then after x the
current subterm will probably be (cons (car a) (append (cdr a) b)) if (consp
a) is among the top-level hypotheses and governors. If there are no top-level
hypotheses and governors, then after x the current subterm will probably
be:
(if (consp a)
(cons (car a) (append (cdr a) b))
b).
General Form:
(X &key
rewrite normalize backchain-limit in-theory hands-off expand)
Expand the function call at the current subterm, and simplify using the
same conventions as with the s command (see ACL2-pc::s).
Unlike s, it is permitted to set both :rewrite and
:normalize to nil, which will result in no simplification; see
ACL2-pc::x-dumb.
Remark (obscure): On rare occasions the current address may be
affected by the use of x. For example, suppose we have the
definition
(defun g (x) (if (consp x) x 3))
and then we enter the interactive proof-builder with
(verify (if (integerp x) (equal (g x) 3) t)) .
Then after invoking the instruction (dive 2 1), so that the current
subterm is (g x), followed by the instruction x, we would expect the
conclusion to be (if (integerp x) (equal 3 3) t). However, the system
actually replaces (equal 3 3) with t (because we use the ACL2
term-forming primitives), and hence the conclusion is actually (if
(integerp x) t t). Therefore, the current address is put at (2) rather
than (2 1). In such cases, a warning ``NOTE'' will be printed to
the terminal.
The other primitive commands to which the above ``truncation'' note applies
are equiv, rewrite, and s.
