		Search-engine friendly clone of the ACL2 documentation.

Base-api

Id-existsp

(id-existsp id aignet) checks whether an ID is in bounds for an aignet.

Executable version of aignet-idp. True iff the ID is less than (num-fanins aignet).

Function: id-existsp

(defun
   aignet$a::id-existsp (id aignet)
   (declare
        (xargs :guard (and (natp id)
                           (aignet$a::aignet-well-formedp aignet))))
   (let ((__function__ 'aignet$a::id-existsp))
        (declare (ignorable __function__))
        (aignet-idp id aignet)))

Function: aignet-idp

(defun aignet-idp (id aignet)
       (declare (xargs :guard (and (natp id) (node-listp aignet))))
       (let ((__function__ 'aignet-idp))
            (declare (ignorable __function__))
            (<= (lnfix id) (fanin-count aignet))))