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
Sv
Vwsim
Fgl
Vl
Syntax
Loader
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Scopestack
Vl-interfaceportlist->ifnames
Vl-blockscope
Vl-scope-find-item
Vl-scopestack-find-item/ss/package
Vl-importlist-find-explicit-item
Vl-scopestack-find-item/context
Vl-importlist-find-implicit-item
Vl-import-stars-find-item
Vl-scopeinfo
Vl-scopeinfo-fix
Vl-scopeinfo-equiv
Make-vl-scopeinfo
Vl-scopeinfo-p
Vl-scopeinfo->star-packages
Vl-scopeinfo->scopetype
Vl-scopeinfo->locals
Vl-scopeinfo->imports
Vl-scopeinfo->id
Change-vl-scopeinfo
Vl-importlist->explicit-item-alist
Vl-scopestack-find-definition/ss
Vl-scopeitem
Vl-scopestack-find-package/ss
Vl-scopestack
Vl-scopeinfo-find-item
Vl-scopestack-find-item/ss
Vl-scopestack-find-class/ss
Scopestack-constants
Vl-scope-namespace
Vl-maybe-scope
Vl-importresult
Vl-scopestack-push
Vl-import-stars-itemnames
Vl-scope->scopeinfo
Vl-scope-find-item-fast
Vl-interface-scope-find-item
Vl-genblob-scope-find-item
Vl-module-scope-find-item
Vl-design-scope-find-definition
Vl-scopestack-find-item
Vl-scopestack-find-definition
Vl-scopeinfo->itemnames
Vl-scope-find-portdecl
Vl-scope-find-definition
Vl-package-scope-find-item
Vl-interface-scope-find-portdecl
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-design-scope-find-class
Vl-class-scope-find-item
Vl-scopestack-find-class
Vl-scope-find-class
Vl-scopestack->hashkey
Vl-scope-find-portdecl-fast
Vl-package-scope-item-alist-top
Vl-scopestack->path-aux
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-scope-find-class-fast
Vl-scope-class-alist
Vl-scopestack->path
Vl-scopestack->design
Vl-scopeitem->name
Vl-scope
Vl-scopestack-init
Vl-importlist->star-packages
Vl-scopestack-pop
Vl-scopestack-nesting-level
Vl-scopestack->toplevel
Vl-scope->scopetype
Vl-scope->id
Vl-design-scope-package-alist-top
Vl-bindlist->modinsts
Vl-scopestack-toplevel-p
Vl-scopestacks-free
Vl-importresult-alist
Hid-tools
Filtering-by-name
Vl-interface-mocktype
Stripping-functions
Genblob
Expr-tools
Extract-vl-types
Hierarchy
Range-tools
Finding-by-name
Stmt-tools
Modnamespace
Flat-warnings
Reordering-by-name
Datatype-tools
Syscalls
Allexprs
Lvalues
Port-tools
Transforms
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 *
id —
vl-maybe-scopeid
scopetype —
vl-scopetype-p
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-p
Recognizer for
vl-scopeinfo
structures.
Vl-scopeinfo->star-packages
Get the
star-packages
field from a
vl-scopeinfo
.
Vl-scopeinfo->scopetype
Get the
scopetype
field from a
vl-scopeinfo
.
Vl-scopeinfo->locals
Get the
locals
field from a
vl-scopeinfo
.
Vl-scopeinfo->imports
Get the
imports
field from a
vl-scopeinfo
.
Vl-scopeinfo->id
Get the
id
field from a
vl-scopeinfo
.
Change-vl-scopeinfo
Modifying constructor for
vl-scopeinfo
structures.