Apply a function symbol or lambda expression to the term, pushing the function into the if branches.
(apply-fn-into-ifs fn term) → new-term
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
Function:
(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)))))))