		Search-engine friendly clone of the ACL2 documentation.

Values

Value-nil

The symbol value for nil.

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

Definitions and Theorems

Function: value-nil

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

Theorem: valuep-of-value-nil

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