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
Preprocessor
Vl-iframe-p
Preprocessor-ifdef-minutia
Vl-preprocess-loop
Vl-read-until-end-of-define
Vl-expand-define
Vl-read-include
Vl-process-ifdef
Vl-substitute-into-macro-text
Vl-preprocess
Vl-define
Vl-define-formallist->defaults
Vl-define-formallist->names
Vl-define-fix
Vl-define-formal
Vl-define-equiv
Make-vl-define
Vl-add-define
Vl-define->formals
Vl-define-p
Change-vl-define
Vl-define->name
Vl-define->loc
Vl-define->body
Vl-pp-define
Vl-define-formallist
Vl-process-define
Vl-process-undef
Preprocessor-include-minutia
Vl-split-define-text
Vl-read-timescale
Vl-line-up-define-formals-and-actuals
Vl-process-else
Vl-process-endif
Vl-istack-p
Vl-is-compiler-directive-p
Vl-check-remaining-formals-all-have-defaults
Vl-safe-previous-n
Vl-safe-next-n
Vl-defines
*vl-preprocess-clock*
Vl-loadconfig
Lexer
Vl-loadstate
Parser
Vl-load-merge-descriptions
Scope-of-defines
Vl-load-file
Vl-flush-out-descriptions
Vl-description
Vl-loadresult
Vl-read-file
Vl-find-basename/extension
Vl-find-file
Vl-read-files
Extended-characters
Vl-load
Vl-load-main
Vl-load-description
Vl-descriptions-left-to-load
Inject-warnings
Vl-load-descriptions
Vl-load-files
Vl-load-summary
Vl-collect-modules-from-descriptions
Vl-descriptionlist
Transforms
Lint
Mlib
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Preprocessor
Vl-define
Internal representation of a
`define
directive.
This is a product type introduced by
defprod
.
Fields
name —
stringp
formals —
vl-define-formallist
Formal arguments to the text macro, if any.
body —
stringp
Macro text associated with this definition. Note that we generally expect this to be trimmed of any whitespace.
loc —
vl-location
Location of this definition in the source code.
Subtopics
Vl-define-formallist->defaults
(vl-define-formallist->defaults x)
maps
vl-define-formal->default
across a list.
Vl-define-formallist->names
(vl-define-formallist->names x)
maps
vl-define-formal->name
across a list.
Vl-define-fix
Fixing function for
vl-define
structures.
Vl-define-formal
A formal argument to a
`define
directive.
Vl-define-equiv
Basic equivalence relation for
vl-define
structures.
Make-vl-define
Basic constructor macro for
vl-define
structures.
Vl-add-define
Add a definition to the defines list.
Vl-define->formals
Get the
formals
field from a
vl-define
.
Vl-define-p
Recognizer for
vl-define
structures.
Change-vl-define
Modifying constructor for
vl-define
structures.
Vl-define->name
Get the
name
field from a
vl-define
.
Vl-define->loc
Get the
loc
field from a
vl-define
.
Vl-define->body
Get the
body
field from a
vl-define
.
Vl-pp-define
Pretty print a
`define
directive.
Vl-define-formallist
A list of
vl-define-formal-p
objects.