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
Scopestack
Vl-interfaceportlist->ifnames
Vl-scope-find-item
Vl-blockscope
Vl-importlist-find-explicit-item
Vl-scopestack-find-item/context
Vl-importlist-find-implicit-item
Vl-import-stars-find-item
Vl-importlist->explicit-item-alist
Vl-scopestack-find-definition/ss
Vl-scopeitem
Vl-scopestack-find-package/ss
Vl-scopeinfo-find-item
Vl-scopestack-find-item/ss
Vl-scopestack
Vl-scopeinfo
Vl-scopeinfo-fix
Vl-scopeinfo-equiv
Make-vl-scopeinfo
Vl-scopeinfo->star-packages
Vl-scopeinfo-p
Vl-scopeinfo->imports
Vl-scopeinfo->locals
Change-vl-scopeinfo
Scopestack-constants
Vl-scopestack-push
Vl-scope->scopeinfo
Vl-scope-find-item-fast
Vl-module-scope-find-item
Vl-importresult
Vl-genblob-scope-find-item
Vl-design-scope-find-definition
Vl-scopestack-find-item
Vl-scopestack-find-definition
Vl-scope-find-portdecl
Vl-scope-find-definition
Vl-package-scope-find-item
Vl-interface-scope-find-portdecl
Vl-interface-scope-find-item
Vl-genblob-scope-find-portdecl
Vl-design-scope-find-item
Vl-blockscope-scope-find-item
Vl-scopestack-find-package
Vl-scope-find-package
Vl-module-scope-find-portdecl
Vl-design-scope-find-package
Vl-scope-find-portdecl-fast
Vl-package-scope-item-alist-top
Vl-scopedef
Vl-scope-portdecl-alist
Vl-scope-package-alist
Vl-scope-find-definition-fast
Vl-scope-definition-alist
Vl-scope-find-package-fast
Vl-scopestack->path-aux
Vl-scopestack->path
Vl-scopestack->design
Vl-scopestack-init
Vl-scopeitem->name
Vl-importlist->star-packages
Vl-scopestack-pop
Vl-scopestack-nesting-level
Vl-scope
Vl-design-scope-package-alist-top
Vl-scopestack-toplevel-p
Vl-scope->name
Vl-scopestacks-free
Vl-importresult-alist
Filtering-by-name
Vl-namefactory
Substitution
Allexprs
Hid-tools
Vl-consteval
Range-tools
Lvalexprs
Hierarchy
Finding-by-name
Expr-tools
Expr-slicing
Stripping-functions
Stmt-tools
Modnamespace
Vl-parse-expr-from-str
Welltyped
Reordering-by-name
Flat-warnings
Genblob
Expr-building
Datatype-tools
Syscalls
Relocate
Expr-cleaning
Namemangle
Caremask
Port-tools
Lvalues
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Scopestack
Vl-scopeinfo
This is a product type introduced by
defprod
.
Fields
locals —
vl-scopeitem-alist
Locally defined names bound to their declarations
imports —
vl-importresult-alist
Explicitly imported names bound to import result, i.e. package-name and declaration)
star-packages —
string-listp
Names of packages imported with *
Subtopics
Vl-scopeinfo-fix
Fixing function for
vl-scopeinfo
structures.
Vl-scopeinfo-equiv
Basic equivalence relation for
vl-scopeinfo
structures.
Make-vl-scopeinfo
Basic constructor macro for
vl-scopeinfo
structures.
Vl-scopeinfo->star-packages
Get the
star-packages
field from a
vl-scopeinfo
.
Vl-scopeinfo-p
Recognizer for
vl-scopeinfo
structures.
Vl-scopeinfo->imports
Get the
imports
field from a
vl-scopeinfo
.
Vl-scopeinfo->locals
Get the
locals
field from a
vl-scopeinfo
.
Change-vl-scopeinfo
Modifying constructor for
vl-scopeinfo
structures.