• 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
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
          • Allexprs
            • Vl-packeddimensionlist-allexprs
            • Vl-namedparamvaluelist-allexprs
            • Vl-paramvaluelist-allexprs
            • Vl-paramdecllist-allexprs
            • Vl-vardecllist-allexprs
            • Vl-taskdecllist-allexprs
            • Vl-portdecllist-allexprs
            • Vl-plainarglist-allexprs
            • Vl-namedarglist-allexprs
            • Vl-modinstlist-allexprs
            • Vl-initiallist-allexprs
            • Vl-gateinstlist-allexprs
            • Vl-fundecllist-allexprs
            • Vl-enumitemlist-allexprs
            • Vl-rangelist-allexprs
            • Vl-modulelist-allexprs
            • Vl-evatomlist-allexprs
            • Vl-assignlist-allexprs
            • Vl-alwayslist-allexprs
            • Vl-aliaslist-allexprs
            • Vl-portlist-allexprs
            • Vl-maybe-delayoreventcontrol-allexprs
            • Vl-maybe-packeddimension-allexprs
            • Vl-delayoreventcontrol-allexprs
            • Vl-repeateventcontrol-allexprs
            • Vl-packeddimension-allexprs
            • Vl-namedparamvalue-allexprs
            • Vl-module-allexprs
            • Vl-maybe-paramvalue-allexprs
            • Vl-maybe-gatedelay-allexprs
            • Vl-paramtype-allexprs
            • Vl-maybe-datatype-allexprs
            • Vl-taskdecl-allexprs
            • Vl-paramvalue-allexprs
            • Vl-paramargs-allexprs
            • Vl-modinst-allexprs
            • Vl-maybe-range-allexprs
            • Vl-maybe-expr-allexprs
            • Vl-gateinst-allexprs
            • Vl-gatedelay-allexprs
            • Vl-fundecl-allexprs
            • Vl-eventcontrol-allexprs
            • Vl-enumitem-allexprs
            • Vl-enumbasetype-allexprs
            • Vl-delaycontrol-allexprs
            • Vl-arguments-allexprs
            • Vl-vardecl-allexprs
            • Vl-portdecl-allexprs
            • Vl-plainarg-allexprs
            • Vl-paramdecl-allexprs
            • Vl-namedarg-allexprs
            • Vl-datatype-allexprs
            • Vl-assign-allexprs
            • Vl-range-allexprs
            • Vl-port-allexprs
            • Vl-initial-allexprs
            • Vl-evatom-allexprs
            • Vl-always-allexprs
            • Vl-alias-allexprs
            • Vl-stmt-allexprs
              • Vl-stmtlist-allexprs
              • Vl-caselist-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
    • Vl-stmt-allexprs

    Vl-caselist-allexprs

    Signature
    (vl-caselist-allexprs x) → exprs
    Arguments
    x — Guard (vl-caselist-p x).
    Returns
    exprs — Type (vl-exprlist-p exprs).