(id->type id aignet) gets the type code of the node with ID
Logically this is
In the execution this is mostly a stobj array lookup in the node array.
Function:
(defun id->type (id aignet) (declare (xargs :stobjs (aignet))) (declare (xargs :guard (natp id))) (declare (xargs :guard (id-existsp id aignet))) (let ((__function__ 'id->type)) (declare (ignorable __function__)) (mbe :logic (non-exec (typecode (ctype (stype (car (lookup-id id aignet)))))) :exec (snode->type^ (id->slot0 id aignet)))))