• 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
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
            • Make-implicit-wires
              • Vl-modulelist-make-implicit-wires
              • Vl-make-implicit-wires-aux
              • Shadowcheck
                • Vl-shadowcheck-reference-name
                • Vl-shadowcheck-aux
                • Vl-shadowcheck-reference-names
                • Vl-shadowcheck-declare-names
                • Vl-shadowcheck-declare-name
                • Vl-shadowcheck-fundecl
                • Vl-shadowcheck-declare-typedefs
                • Vl-shadowcheck-blockitemlist
                • Vl-shadowcheck-taskdecl
                • Vl-shadowcheck-portdecllist
                • Vl-shadowcheck-paramdecls
                • Vl-shadowcheck-taskdecls
                • Vl-shadowcheck-paramdecl
                • Vl-shadowcheck-gateinst
                • Vl-shadowcheck-vardecls
                • Vl-shadowcheck-vardecl
                • Vl-shadowcheck-portdecl
                • Vl-shadowcheck-modinst
                • Vl-shadowcheck-imports
                • Vl-shadowcheck-import
                • Vl-shadowcheck-fundecls
                • Vl-shadowcheck-blockitem
                • Vl-shadowcheck-ports
                • Vl-shadowcheck-port
                • Vl-shadowcheck-initial
                • Vl-shadowcheck-assign
                • Vl-shadowcheck-always
                • Vl-shadowcheck-alias
                • Vl-shadowcheck-state
                • Vl-shadowcheck-module
                • Vl-shadowcheck-modules
                • Vl-shadowcheck-push-scope
                • Vl-lexscopes
                  • Vl-lexscopes-fix
                  • Vl-lexscopes-direct-import-name
                  • Vl-lexscopes-wild-import-name
                  • Vl-lexscopes-wild-import-names
                  • Vl-lexscopes-declare-name
                  • Vl-lexscopes-do-import
                  • Vl-lexscopes-find
                  • Vl-lexscopes-equiv
                  • Vl-lexscopes-p
                  • Vl-lexscopes-exit-scope
                  • Vl-lexscopes-enter-new-scope
                • Vl-shadowcheck-design
                • Vl-shadowcheck-pop-scope
                • Vl-lexscope
              • Vl-stmt-check-undeclared
              • Vl-make-implicit-wires-main
              • Vl-fundecl-check-undeclared
              • Vl-warn-about-undeclared-wires
              • Vl-implicitst
              • Vl-blockitem-check-undeclared
              • Vl-taskdecl-check-undeclared
              • Vl-modinst-exprs-for-implicit-wires
              • Vl-blockitemlist-check-undeclared
              • Vl-import-check-undeclared
              • Vl-make-ordinary-implicit-wires
              • Vl-gateinst-exprs-for-implicit-wires
              • Vl-remove-declared-wires
              • Vl-make-port-implicit-wires
              • Vl-module-make-implicit-wires
              • Vl-vardecl-exprs-for-implicit-wires
              • Vl-design-make-implicit-wires
            • Resolve-indexing
            • Origexprs
            • Argresolve
            • Portdecl-sign
            • Designwires
            • Udp-elim
            • Vl-annotate-design
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Vwsim
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Shadowcheck

Vl-lexscopes

A stack of lexical scopes.

This is an ordinary fty::deflist.

Subtopics

Vl-lexscopes-fix
(vl-lexscopes-fix x) is a usual ACL2::fty list fixing function.
Vl-lexscopes-direct-import-name
Extend the lexscopes with a direct import of a single name.
Vl-lexscopes-wild-import-name
Extend the lexscopes with a wildcard import of a single name.
Vl-lexscopes-wild-import-names
Extend the lexscopes with a wildcard import of a list of names.
Vl-lexscopes-declare-name
Extend the lexscopes with a local declaration.
Vl-lexscopes-do-import
Extend the lexscopes with a package import.
Vl-lexscopes-find
Recursively look up a name, going from inner to outer lexical scopes.
Vl-lexscopes-equiv
Basic equivalence relation for vl-lexscopes structures.
Vl-lexscopes-p
(vl-lexscopes-p x) recognizes lists where every element satisfies vl-lexscope-p.
Vl-lexscopes-exit-scope
Pop the current scope off of the lexical scope stack and free fast alists.
Vl-lexscopes-enter-new-scope
Push a new scope onto the lexical scope stack.