		Search-engine friendly clone of the ACL2 documentation.

Pointer-operations

Value-pointer-null

Null pointer for a given referenced type.

Signature
(value-pointer-null reftype) → ptr
Arguments: reftype — Guard (typep reftype).
Returns: ptr — Type (valuep ptr).

Definitions and Theorems

Function: value-pointer-null

(defun value-pointer-null (reftype)
  (declare (xargs :guard (typep reftype)))
  (let ((__function__ 'value-pointer-null))
    (declare (ignorable __function__))
    (make-value-pointer :core (pointer-null)
                        :reftype reftype)))

Theorem: valuep-of-value-pointer-null

(defthm valuep-of-value-pointer-null
  (b* ((ptr (value-pointer-null reftype)))
    (valuep ptr))
  :rule-classes :rewrite)

Theorem: value-kind-of-value-pointer-null

(defthm value-kind-of-value-pointer-null
  (b* ((?ptr (value-pointer-null reftype)))
    (equal (value-kind ptr) :pointer)))

Theorem: value-pointer-null-of-type-fix-reftype

(defthm value-pointer-null-of-type-fix-reftype
  (equal (value-pointer-null (type-fix reftype))
         (value-pointer-null reftype)))

Theorem: value-pointer-null-type-equiv-congruence-on-reftype

(defthm value-pointer-null-type-equiv-congruence-on-reftype
  (implies (type-equiv reftype reftype-equiv)
           (equal (value-pointer-null reftype)
                  (value-pointer-null reftype-equiv)))
  :rule-classes :congruence)