• 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
          • Hid-tools
          • Filtering-by-name
          • Vl-interface-mocktype
          • Stripping-functions
          • Genblob
          • Expr-tools
          • Extract-vl-types
          • Hierarchy
          • Range-tools
          • Finding-by-name
          • Stmt-tools
            • Vl-rebuild-caselist
            • Vl-stmt-atomicstmts
              • Vl-stmtlist-atomicstmts
                • Vl-stmt-atomicstmts-nrev
              • Vl-compoundstmt->stmts
              • Vl-compoundstmt->exprs
              • Vl-compoundstmt->vardecls
              • Change-vl-compoundstmt
              • Vl-compoundstmt->paramdecls
              • Vl-compoundstmt->ctrl
              • Vl-atomicstmtlist-p
              • Vl-stmt->atts
              • Vl-atomicstmt-p
              • Vl-timingstmt-p
              • Vl-repeatstmt-p
              • Vl-foreverstmt-p
              • Vl-assignstmt-p
              • Vl-whilestmt-p
              • Vl-waitstmt-p
              • Vl-nullstmt-p
              • Vl-ifstmt-p
              • Vl-forstmt-p
              • Vl-dostmt-p
              • Vl-casestmt-p
              • Vl-callstmt-p
              • Vl-exprlistlist
            • Modnamespace
            • Flat-warnings
            • Reordering-by-name
            • Datatype-tools
            • Syscalls
            • Allexprs
            • Lvalues
            • Port-tools
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-stmt-atomicstmts

    Vl-stmtlist-atomicstmts

    Signature
    (vl-stmtlist-atomicstmts x) → stmts
    Arguments
    x — Guard (vl-stmtlist-p x).
    Returns
    stmts — Type (and (vl-stmtlist-p stmts) (vl-atomicstmtlist-p stmts)).