		Search-engine friendly clone of the ACL2 documentation.

Values

Lower-value

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

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

This is the inverse of lift-value.

Definitions and Theorems

Function: lower-value

(defun
 lower-value (xval)
 (declare (xargs :guard (valuep xval)))
 (let
    ((__function__ 'lower-value))
    (declare (ignorable __function__))
    (value-case xval
                :number (value-number->get xval)
                :character (value-character->get xval)
                :string (value-string->get xval)
                :symbol (lower-symbol (value-symbol->get xval))
                :cons (cons (lower-value (value-cons->car xval))
                            (lower-value (value-cons->cdr xval))))))

Theorem: good-valuep-of-lower-value

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

Theorem: lower-value-of-value-fix-xval

(defthm lower-value-of-value-fix-xval
        (equal (lower-value (value-fix xval))
               (lower-value xval)))

Theorem: lower-value-value-equiv-congruence-on-xval

(defthm lower-value-value-equiv-congruence-on-xval
        (implies (value-equiv xval xval-equiv)
                 (equal (lower-value xval)
                        (lower-value xval-equiv)))
        :rule-classes :congruence)