		Search-engine friendly clone of the ACL2 documentation.

Pseudo-term-fty

Pseudo-term-null

Constructor for null pseudo-terms. Just returns NIL.

Signature
(pseudo-term-null) → term
Returns: term — Type (pseudo-termp term).

Definitions and Theorems

Function: pseudo-term-null

(defun pseudo-term-null nil
  (declare (xargs :guard t))
  (let ((__function__ 'pseudo-term-null))
    (declare (ignorable __function__))
    nil))

Theorem: pseudo-termp-of-pseudo-term-null

(defthm pseudo-termp-of-pseudo-term-null
  (b* ((term (pseudo-term-null)))
    (pseudo-termp term))
  :rule-classes :rewrite)

Theorem: kind-of-pseudo-term-null

(defthm kind-of-pseudo-term-null
  (equal (pseudo-term-kind (pseudo-term-null))
         :null))

Theorem: base-ev-of-pseudo-term-null

(defthm base-ev-of-pseudo-term-null
  (equal (base-ev (pseudo-term-null) a)
         nil))

Theorem: base-ev-when-pseudo-term-null

(defthm base-ev-when-pseudo-term-null
  (implies (equal (pseudo-term-kind x) :null)
           (equal (base-ev x a) nil)))

Theorem: pseudo-term-fix-when-pseudo-term-null

(defthm pseudo-term-fix-when-pseudo-term-null
  (implies (equal (pseudo-term-kind x) :null)
           (equal (pseudo-term-fix x)
                  (pseudo-term-null))))

Subtopics

Pseudo-term-const->val: Accessor for the value of a null or quote pseudo-term.