		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Internal representation of a `define directive.

This is a product type introduced by defprod.

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.
stickyp — booleanp: Is this define "sticky". If so, and we encounter another `define of name, then we keep the old definition instead of redefining it. This is similar to how other tools treat command-line +define options; see the defines cosim for more details.

Vl-define-formallist->names: (vl-define-formallist->names x) maps vl-define-formal->name across a list.
Vl-parse-cmdline-define: Essentially treats "foo" like `define foo, or "foo=3" like `define foo 3`.
Vl-parse-cmdline-defines-aux
Vl-parse-cmdline-defines
Vl-define-fix: Fixing function for vl-define structures.
Vl-maybe-define: Option type; vl-define or nil.
Vl-define-formal: A formal argument to a `define directive.
Vl-make-initial-defines: Simple way to build a vl-defines-p that `defines a list of names to 1.
Vl-add-define: Add a definition to the defines list.
Vl-define-equiv: Basic equivalence relation for vl-define structures.
Make-vl-define: Basic constructor macro for vl-define structures.
Vl-pp-define: Pretty print a `define directive.
Vl-delete-define: Delete an entry from the defines list, if it exists.
Vl-find-define: Look up a definition in the defines list.
Vl-define->formals: Get the formals field from a vl-define.
Vl-define->stickyp: Get the stickyp field from a vl-define.
Change-vl-define: Modifying constructor for vl-define structures.
Vl-define->loc: Get the loc field from a vl-define.
Vl-define->body: Get the body field from a vl-define.
Vl-define-p: Recognizer for vl-define structures.
Vl-defines->names
Vl-define-formallist: A list of vl-define-formal-p objects.