		Search-engine friendly clone of the ACL2 documentation.

Base-api

Id->regp

(id->regp id aignet) gets the register bit from the node with ID id.

Logically this is (regp (stype (car (lookup-id id aignet)))).

In the execution this is mostly a stobj array lookup in the node array.

Function: id->regp

(defun id->regp (id aignet)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (natp id)))
 (declare (xargs :guard (id-existsp id aignet)))
 (let ((__function__ 'id->regp))
   (declare (ignorable __function__))
   (mbe :logic (non-exec (regp (stype (car (lookup-id id aignet)))))
        :exec (snode->regp^ (id->slot1 id aignet)))))