		Search-engine friendly clone of the ACL2 documentation.

Pointer-operations

Value-pointer-nullp

Check if a pointer is null.

Signature
(value-pointer-nullp ptr) → yes/no
Arguments: ptr — Guard (valuep ptr).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: value-pointer-nullp

(defun value-pointer-nullp (ptr)
  (declare (xargs :guard (valuep ptr)))
  (declare (xargs :guard (value-case ptr :pointer)))
  (let ((__function__ 'value-pointer-nullp))
    (declare (ignorable __function__))
    (pointer-case (value-pointer->core ptr)
                  :null)))

Theorem: booleanp-of-value-pointer-nullp

(defthm booleanp-of-value-pointer-nullp
  (b* ((yes/no (value-pointer-nullp ptr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: value-pointer-nullp-of-value-pointer

(defthm value-pointer-nullp-of-value-pointer
  (equal (value-pointer-nullp (value-pointer core type))
         (pointer-case core :null)))

Theorem: value-pointer-nullp-of-value-fix-ptr

(defthm value-pointer-nullp-of-value-fix-ptr
  (equal (value-pointer-nullp (value-fix ptr))
         (value-pointer-nullp ptr)))

Theorem: value-pointer-nullp-value-equiv-congruence-on-ptr

(defthm value-pointer-nullp-value-equiv-congruence-on-ptr
  (implies (value-equiv ptr ptr-equiv)
           (equal (value-pointer-nullp ptr)
                  (value-pointer-nullp ptr-equiv)))
  :rule-classes :congruence)