• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
          • Alias-normalization
          • Svex-design-flatten-and-normalize
          • Svex-design-compile
          • Svex-composition
            • Svex-compose-assigns-keys
            • Svex-compose*
            • Svex-compose
              • Svexlist-compose
              • Svex-compose-svstack
              • Svex-assigns-compose1
              • Svex-assigns-compose
              • Svex-compose-bit-sccs
              • Svex-compose-assigns
              • Svex-replace-var
            • Compile.lisp
            • Assign->segment-drivers
            • Segment-driver-map-resolve
            • Assigns->segment-drivers
          • Moddb
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Vwsim
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Svex-compose

    Svexlist-compose

    Signature
    (svexlist-compose x a) → xa
    Arguments
    x — Guard (svexlist-p x).
    a — Guard (svex-alist-p a).
    Returns
    xa — Type (svexlist-p xa).