• 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
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
          • 4vec
            • 4vec-operations
            • 4vec-p
            • S4vecs
              • S4vec-p
              • S4vec-part-install
              • S4vec-?!
              • S4vec-fix
              • S4vec-rev-blocks
              • Sparseint-rev-blocks
              • S4vec-part-select
              • S3vec-bit?
              • S4vec-concat
              • S4vec-bitmux
              • S4vec-bit?!
              • S3vec-?*
              • S3vec-?
              • Svex-s4apply
              • S4vec-bit?
              • S4vec-?*
              • S4vec-?
              • S4vec-===*
              • S4vec-pow
              • S4vec
              • S4vec-sign-ext
              • S4vec-override
              • S4vec-zero-ext
              • S4vec-wildeq-safe
              • S4vec-symwildeq
              • S4vec-shift-core
              • S4vec-remainder
              • S4vec-quotient
              • S4vec-bitxor
              • S3vec-bitxor
              • S4vec-resor
              • S4vec-resand
              • S4vec-bit-index
              • S4vec-bit-extract
              • S3vec-bitor
              • S3vec-bitand
              • S4vec->4vec
              • S4vec-wildeq
              • S4vec-times
              • S4vec-rsh
              • S4vec-plus
              • S4vec-minus
              • S4vec-bitand
              • S4vec-===
              • S4vec-<
              • S4vec-res
              • S4vec-lsh
              • S4vec-bitor
              • S4vec-==
              • S3vec-==
              • S4vec-equal
              • S3vec-reduction-or
              • S3vec-reduction-and
              • S4vec-sparseint-val
              • S4vec-parity
              • S4vec-countones
              • S2vec
              • S4vec-reduction-or
              • S4vec-reduction-and
              • S4vec-onehot0
              • S4vec-onehot
              • S4vec-offset
              • S3vec-bitnot
              • 4vec->s4vec
              • S4vec-xdet
              • S4vec-uminus
              • S4vec-onset
              • S4vec-clog2
              • S4vec-bitnot
              • S4vec-1mask
              • S3vec-fix
              • S4vec->upper
              • S4vec->lower
              • S4vec-index-p
              • S4veclist
                • S4veclist-fix
                • S4veclist-nth-safe
                • S4veclist-equiv
                • S4veclist-p
              • S4vec-xfree-p
              • S4vec-2vec-p
              • S3vec-p
              • S2vec->val
              • S2vec-p
              • S4vec-correct-fn
              • S4vec-correct-formal-evals
            • 4vec-examples
            • Maybe-4vec
            • 4vec-equiv
            • Make-4vec
            • 4vec->upper
            • 4vec->lower
            • 4veclist
            • 4vec-fix
            • Make-honsed-4vec
            • 4vec-index-p
          • 4vec-<<=
          • 3vec
          • 2vec
          • 2vecx
          • 2vecnatx
          • 4vec-x
          • 4vec-1x
          • 4vec-1z
          • 4vec-z
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• S4vecs

S4veclist

A list of s4vec-p objects.

This is an ordinary deflist.

Subtopics

S4veclist-fix

(s4veclist-fix x) is a usual fty list fixing function.

S4veclist-nth-safe

Like nth but, with proper fty-discipline for s4veclists. ``Safely'' causes a run-time error if n is out of bounds.

S4veclist-equiv

Basic equivalence relation for s4veclist structures.

S4veclist-p

(s4veclist-p x) recognizes lists where every element satisfies s4vec-p.