		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)