		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::expand

(primitive) expand the current function call without simplification

Examples:
expand -- expand and do not simplify.

Also see ACL2-pc::x, which performs simplification, and see ACL2-pc::x-dumb, which provides a simple interface to acl2-pc::expand.

For example, if the current subterm is (append a b), then after expand the current subterm will be the term:

(if (consp a)
    (cons (car a) (append (cdr a) b))
  b)

regardless of the top-level hypotheses and the governors.

General Form:
(expand &optional do-not-expand-lambda-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