		Search-engine friendly clone of the ACL2 documentation.

Base-api

Id->type

(id->type id aignet) gets the type code of the node with ID id.

Logically this is (node->type (car (lookup-id id aignet))).

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

Function: id->type

(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)))))