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 expressionSee also
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
x, which allows simplification.