		Search-engine friendly clone of the ACL2 documentation.

Base-api

Outnum->fanin

(outnum->fanin n aignet) gets the fanin literal of primary output number n.

Logically this is (fanin 0 (lookup-stype n :po aignet)).

In the execution this is a stobj array lookup in the outputs array.

Function: outnum->fanin

(defun aignet$a::outnum->fanin (out aignet)
  (declare
       (xargs :guard (and (natp out)
                          (aignet$a::aignet-well-formedp aignet))))
  (declare (xargs :guard (< out (aignet$a::num-outs aignet))))
  (let ((__function__ 'aignet$a::outnum->fanin))
    (declare (ignorable __function__))
    (fanin 0 (lookup-stype out :po aignet))))