		Search-engine friendly clone of the ACL2 documentation.

Pointers

New-pointer

Obtain a new Java pointer.

Signature
(new-pointer pointers) → pointer
Arguments: pointers — Guard (pointer-listp pointers).
Returns: pointer — Type (pointerp pointer).

See pointerp for details on how new pointers are obtained. This function is a guarded wrapper of the constrained function new-pointer-raw introduced with pointerp.

Definitions and Theorems

Function: new-pointer

(defun new-pointer (pointers)
  (declare (xargs :guard (pointer-listp pointers)))
  (let ((__function__ 'new-pointer))
    (declare (ignorable __function__))
    (new-pointer-raw pointers)))

Theorem: pointerp-of-new-pointer

(defthm pointerp-of-new-pointer
  (b* ((pointer (new-pointer pointers)))
    (pointerp pointer))
  :rule-classes :rewrite)

Theorem: new-pointer-is-new

(defthm new-pointer-is-new
  (not (member-equal (new-pointer pointers)
                     pointers)))