		Search-engine friendly clone of the ACL2 documentation.

Parser-output-to-abstract-syntax

Value-irrelevant

An irrelevant JSON value.

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

Definitions and Theorems

Function: value-irrelevant

(defun
 value-irrelevant
 nil (declare (xargs :guard t))
 (let
     ((__function__ 'value-irrelevant))
     (declare (ignorable __function__))
     (with-guard-checking :none (ec-call (value-fix :irrelevant)))))

Theorem: valuep-of-value-irrelevant

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