Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Ipasir
Aignet
Base-api
Aignet-construction
Representation
Aignet-impl
Node
Network
Lookup-id
Lookup-stype
Aignet-extension-p
Aignet-nodes-ok
Aignet-outputs-aux
Aignet-nxsts-aux
Fanin
Aignet-outputs
Lookup-reg->nxst
Aignet-lit-fix
Aignet-fanins
Stype-count
Aignet-nxsts
Aignet-idp
Aignet-norm
Aignet-norm-p
Aignet-id-fix
Fanin-count
Proper-node-listp
Fanin-node-p
Node-list
Node-list-fix
Node-listp
Node-list-equiv
Aignet-litp
Combinational-type
Typecode
Stypep
Aignet-copy-init
Aignet-simplify-with-tracking
Aignet-simplify-marked-with-tracking
Aignet-cnf
Aignet-simplify-marked
Aignet-complete-copy
Aignet-transforms
Aignet-eval
Semantics
Aignet-read-aiger
Aignet-write-aiger
Aignet-abc-interface
Utilities
Aig
Satlink
Truth
Ubdds
Bdd
Faig
Bed
4v
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Network
Node-list
A list of
node-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Node-list-fix
(node-list-fix x)
is a usual
ACL2::fty
list fixing function.
Node-listp
(node-listp x)
recognizes lists where every element satisfies
node-p
.
Node-list-equiv
Basic equivalence relation for
node-list
structures.