		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)