		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Apply-fn-into-ifs

Apply a function symbol or lambda expression to the term, pushing the function into the if branches.

Signature
(apply-fn-into-ifs fn term) → new-term
Arguments: fn — Guard (pseudo-termfnp fn).; term — Guard (pseudo-termp term).
Returns: new-term — A pseudo-termp.

If the term is not an if, the function is applied to the term. Otherwise, the function is applied to the `then' and `else' branches, and recursively to their `then' and `else' branches if those are ifs as well. For instance, applying a symbol f to (if a (if b c d) e) results in (if a (if b (f c) (f d)) (f e)).

Definitions and Theorems

Function: apply-fn-into-ifs

(defun apply-fn-into-ifs (fn term)
 (declare (xargs :guard (and (pseudo-termfnp fn)
                             (pseudo-termp term))))
 (declare (xargs :guard (or (symbolp fn)
                            (= (len (lambda-formals fn)) 1))))
 (let ((__function__ 'apply-fn-into-ifs))
  (declare (ignorable __function__))
  (b*
   (((when (variablep term))
     (apply-term* fn term))
    ((when (fquotep term))
     (apply-term* fn term))
    ((unless (eq (ffn-symb term) 'if))
     (apply-term* fn term))
    ((unless (= (len (fargs term)) 3))
     (raise
      "Internal error: ~
                the IF term ~x0 does not have 3 arguments."
      term)))
   (cons-term 'if
              (list (fargn term 1)
                    (apply-fn-into-ifs fn (fargn term 2))
                    (apply-fn-into-ifs fn (fargn term 3)))))))