		Search-engine friendly clone of the ACL2 documentation.

Values

Value-t

The symbol value for t.

Signature
(value-t) → value
Returns: value — Type (valuep value).

Definitions and Theorems

Function: value-t

(defun value-t nil
  (declare (xargs :guard t))
  (let ((__function__ 'value-t))
    (declare (ignorable __function__))
    (value-symbol (lift-symbol t))))

Theorem: valuep-of-value-t

(defthm valuep-of-value-t
  (b* ((value (value-t))) (valuep value))
  :rule-classes :rewrite)