Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Warnings
Primitives
Use-set
Syntax
Getting-started
Utilities
Loader
Transforms
Lint
Mlib
Server
Kit
Printer
Ps
Basic-printing
Verilog-printing
Vl-fmt
Vl-ppc-module
Vl-pp-expr
Vl-pp-exprlist
Vl-pp-atts-aux
Vl-pp-atts
Vl-maybe-escape-identifier
Vl-print-ext-wirename
Vl-pp-module
Vl-print-wirename
Vl-print-loc
Vl-print-modname
Vl-pp-origexpr
Vl-pps-module
Vl-pps-expr
Vl-ppc-modulelist
Vl-ppcs-module
Vl-ps-update-show-atts
Vl-pps-origexpr
Vl-pps-modulelist
Vl-ppcs-modulelist
Vl-cw-obj
Vl-ps->show-atts-p
Vl-cw
Printing-locally
Formatted-printing
Accessing-printed-output
Vl-printedlist
Json-printing
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-pp-expr
Vl-pp-atts-aux
Signature
(vl-pp-atts-aux x &key (ps 'ps)) → ps
Arguments
x
—
Guard
(
vl-atts-p
x)
.