Lift a defined function from the current ACL2 environment to the meta level.
This must be used only on function symbols with an unnormalized body property. Otherwise, this causes an error.
If those conditions hold, we retrieve the function's formal parameters and (unnormalized) body, and we lift them to the meta level together with the name.
(defun lift-function (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'lift-function)) (declare (ignorable __function__)) (b* (((when (not (function-symbolp fn wrld))) (raise "The symbol ~x0 does not name a function." fn) (ec-call (function-fix :irrelevant))) (params (formals+ fn wrld)) (body (ubody+ fn wrld)) ((unless (good-pseudo-termp body)) (raise "Internal error: the term ~x0 is not good." body) (ec-call (function-fix :irrelevant))) ((when (null body)) (raise "The function ~x0 has no unnormalized body." fn) (ec-call (function-fix :irrelevant)))) (make-function :name (lift-symbol fn) :params (lift-symbol-list params) :body (lift-term body)))))
(defthm functionp-of-lift-function (b* ((function (lift-function fn wrld))) (functionp function)) :rule-classes :rewrite)