• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
        • E-conversion
          • Vl-ealist-p
          • Modinsts-to-eoccs
          • Vl-module-make-esim
          • Exploding-vectors
            • Vl-wirealist-p
            • Emodwire-encoding
            • Vl-emodwire-p
            • Vl-emodwirelistlist
            • Vl-emodwirelist
              • Vl-emodwirelist-fix
              • Vl-emodwirelist-p
                • Vl-emodwirelist-p-basics
              • Vl-emodwirelist-equiv
          • Resolving-multiple-drivers
          • Vl-modulelist-make-esims
          • Vl-module-check-e-ok
          • Vl-collect-design-wires
          • Adding-z-drivers
          • Vl-design-to-e
          • Vl-design-to-e-check-ports
          • Vl-design-to-e-main
          • Port-bit-checking
        • Esim-steps
        • Patterns
        • Mod-internal-paths
        • Defmodules
        • Esim-simplify-update-fns
        • Esim-tutorial
        • Esim-vl
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-emodwirelist

Vl-emodwirelist-p

(vl-emodwirelist-p x) recognizes lists where every element satisfies vl-emodwire-p.

Signature
(vl-emodwirelist-p x) → *

This is an ordinary deflist. It is "loose" in that it does not care whether x is nil-terminated.

Subtopics

Vl-emodwirelist-p-basics
Basic theorems about vl-emodwirelist-p, generated by deflist.