		Search-engine friendly clone of the ACL2 documentation.

Pointer-operations

Value-pointer->designator

Object designator of a valid pointer.

Signature
(value-pointer->designator ptr) → design
Arguments: ptr — Guard (valuep ptr).
Returns: design — Type (objdesignp design).

Definitions and Theorems

Function: value-pointer->designator

(defun value-pointer->designator (ptr)
  (declare (xargs :guard (valuep ptr)))
  (declare (xargs :guard (and (value-case ptr :pointer)
                              (value-pointer-validp ptr))))
  (let ((__function__ 'value-pointer->designator))
    (declare (ignorable __function__))
    (pointer-valid->get (value-pointer->core ptr))))

Theorem: objdesignp-of-value-pointer->designator

(defthm objdesignp-of-value-pointer->designator
  (b* ((design (value-pointer->designator ptr)))
    (objdesignp design))
  :rule-classes :rewrite)

Theorem: value-pointer->designator-of-value-pointer

(defthm value-pointer->designator-of-value-pointer
  (equal (value-pointer->designator (value-pointer core type))
         (pointer-valid->get core)))

Theorem: value-pointer->designator-of-value-fix-ptr

(defthm value-pointer->designator-of-value-fix-ptr
  (equal (value-pointer->designator (value-fix ptr))
         (value-pointer->designator ptr)))

Theorem: value-pointer->designator-value-equiv-congruence-on-ptr

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