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