• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
            • Vl-expr-expand-function-calls
            • Vl-expand-function-call
            • Vl-module-expand-functions
            • Vl-modulelist-expand-functions
            • Vl-check-bad-funcalls
            • Vl-funtemplate
              • Vl-funtemplate-p
                • Vl-fun-vardecllist-to-vardecls
                • Vl-funinputlist-to-vardecls
                • Vl-fundecl-expansion-template
                • Vl-funinput-to-vardecl
                • Vl-fundecllist-expansion-templates
                • Vl-fun-vardecllist-types-okp
                • Vl-portdecllist-types-okp
                • Vl-fun-vardecl-to-vardecl
                • Vl-find-funtemplate
                • Vl-funtemplatelist
                  • Vl-funtemplatelist-fix
                  • Vl-funtemplatelist-equiv
                  • Vl-funtemplatelist-p
                    • Vl-funtemplatelist-p-basics
              • Vl-funtemplate-fix
              • Vl-funtemplate-equiv
              • Make-vl-funtemplate
              • Vl-funtemplate->locals
              • Vl-funtemplate->inputs
              • Vl-funtemplate->assigns
              • Change-vl-funtemplate
              • Vl-funtemplate->out
              • Vl-funtemplate->name
            • Vl-funbody-to-assignments
            • Vl-assignlist->rhses
            • Vl-fundecl-expand-params
            • Vl-fun-stmt-okp
            • Vl-fundecllist-expand-params
            • Vl-remove-fake-function-vardecls
            • Vl-design-expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-funtemplatelist

Vl-funtemplatelist-p

(vl-funtemplatelist-p x) recognizes lists where every element satisfies vl-funtemplate-p.

Signature
(vl-funtemplatelist-p x) → *

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

Subtopics

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