		Search-engine friendly clone of the ACL2 documentation.

Programs

Lift-program

Lift a program from the current ACL2 environment to the meta level.

Signature
(lift-program fns state) → program
Arguments: fns — Guard (symbol-listp fns).
Returns: program — Type (programp program).

We lift all the known packages, along with the functions specified by symbol. In general there are too many functions in the ACL2 environment, so we only lift the specified functions. Care must be exercised so that the list of functions is closed with respect to calls.

Definitions and Theorems

Function: lift-program

(defun lift-program (fns state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (symbol-listp fns)))
  (let ((__function__ 'lift-program))
    (declare (ignorable __function__))
    (b* ((packages (lift-package-list (known-packages+ state)))
         (functions (lift-function-list fns (w state))))
      (make-program :packages packages
                    :functions functions))))

Theorem: programp-of-lift-program

(defthm programp-of-lift-program
  (b* ((program (lift-program fns state)))
    (programp program))
  :rule-classes :rewrite)