• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • 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-emodwirelistlist-fix
              • Vl-emodwirelistlist-equiv
              • Vl-emodwirelistlist-p
                • Vl-emodwirelistlist-p-basics
            • Vl-emodwirelist
          • 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
      • Vwsim
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Vl-emodwirelistlist

Vl-emodwirelistlist-p

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

Signature
(vl-emodwirelistlist-p x) → *

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

Subtopics

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