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