ACL2-PC::EXPAND

(primitive) expand the current function call without simplification
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
expand -- expand and do not simplify.
For example, if the current subterm is (append a b), then after (expand t) the current subterm will be the term:
(if (true-listp x)
    (if x
        (cons (car x) (append (cdr x) y))
      y)
  (apply 'binary-append (list x y)))
regardless of the top-level hypotheses and the governors.

General Form:
(expand &optional
        do-not-expand-lambda-flg new-goals-flg keep-all-guards-flg)
Expand the function call at the current subterm, and do not simplify. The options have the following meanings:
do-not-expand-lambda-flg:   default is nil; otherwise, the result
                            should be a lambda expression

new-goals-flg: default of nil means to introduce APPLY for guards

keep-all-guards-flg: default of nil means that the system should make a weak attempt to prove the guards from the current context

See also x, which allows simplification.