		Search-engine friendly clone of the ACL2 documentation.

Values

Lift-value

Lift an ACL2 good value to a meta-level value.

Signature
(lift-value x) → xval
Arguments: x — Guard (good-valuep x).
Returns: xval — Type (valuep xval).

This extends lift-symbol to all values. More precisely, to all ``good'' values, as captured by good-valuep. Even though good values are the only ones possible in execution, from a logical point of view there may be other values (i.e. bad atoms or cons pairs containing bad atoms at some level), and thus we need to restrict the domain of this lifting function.

Definitions and Theorems

Function: lift-value

(defun lift-value (x)
       (declare (xargs :guard (good-valuep x)))
       (let ((__function__ 'lift-value))
            (declare (ignorable __function__))
            (cond ((consp x)
                   (value-cons (lift-value (car x))
                               (lift-value (cdr x))))
                  ((acl2-numberp x) (value-number x))
                  ((characterp x) (value-character x))
                  ((stringp x) (value-string x))
                  ((symbolp x)
                   (value-symbol (lift-symbol x)))
                  (t (prog2$ (impossible)
                             (ec-call (value-fix :irrelevant)))))))

Theorem: valuep-of-lift-value

(defthm valuep-of-lift-value
        (b* ((xval (lift-value x)))
            (valuep xval))
        :rule-classes :rewrite)