		Search-engine friendly clone of the ACL2 documentation.

Functions

Lift-function

Lift a defined function from the current ACL2 environment to the meta level.

Signature
(lift-function fn wrld) → function
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: function — Type (functionp function).

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.

Definitions and Theorems

Function: lift-function

(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)))))

Theorem: functionp-of-lift-function

(defthm functionp-of-lift-function
  (b* ((function (lift-function fn wrld)))
    (functionp function))
  :rule-classes :rewrite)