• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-fixpoint-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
          • Svexlist-compose-dfs
          • Moddb
          • Svex-compilation
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Vwsim
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Svex-compose-dfs

    Svexlist-compose-dfs

    Signature
    (svexlist-compose-dfs x assigns updates memo stack) 
  → 
(mv x1 updates1 memo1)
    Arguments
    x — Guard (svexlist-p x).
    assigns — Guard (svex-alist-p assigns).
    updates — Guard (svex-alist-p updates).
    memo — Guard (svex-svex-memo-p memo).
    stack — Guard (alistp stack).
    Returns
    x1 — Type (svexlist-p x1).
    updates1 — Type (svex-alist-p updates1).
    memo1 — Type (svex-svex-memo-p memo1).