		Search-engine friendly clone of the ACL2 documentation.

Base-api

Aignet-add-in

(aignet-add-in aignet) adds a new primary input node to the aignet.

Logically this is just (cons (pi-node) aignet).

In the execution we update the necessary arrays, counts, etc.

Function: aignet-add-in^

(defun
     aignet$a::aignet-add-in^ (aignet)
     (declare (xargs :guard (aignet$a::aignet-well-formedp aignet)))
     (declare (xargs :guard (< (aignet$a::num-fanins aignet)
                               536870911)))
     (let ((__function__ 'aignet$a::aignet-add-in^))
          (declare (ignorable __function__))
          (cons (pi-node)
                (node-list-fix aignet))))