• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
          • Name-database
          • Vl-gc
          • Symbol-list-names
          • Ints-from
          • Nats-from
          • Make-lookup-alist
          • Redundant-mergesort
          • Longest-common-prefix
          • Vl-remove-keys
          • Vl-plural-p
          • Vl-merge-contiguous-indices
          • Sum-nats
          • Vl-edition-p
          • Vl-maybe-integer-listp
          • Fast-memberp
          • Nat-listp
          • Max-nats
          • Longest-common-prefix-list
          • Character-list-listp
          • Vl-character-list-list-values-p
          • Remove-from-alist
          • Prefix-of-eachp
          • Vl-string-keys-p
          • Vl-maybe-nat-listp
          • Vl-string-list-values-p
          • String-list-listp
          • Vl-string-values-p
          • Explode-list
          • True-list-listp
          • Symbol-list-listp
          • All-have-len
          • Pos-listp
          • Min-nats
          • Debuggable-and
          • Vl-starname
          • Remove-equal-without-guard
          • String-fix
          • Anyp
          • Vl-maybe-string-list
            • Vl-maybe-string-list-fix
            • Vl-maybe-string-list-equiv
            • Vl-maybe-string-list-p
          • Longer-than-p
          • Fast-alist-free-each-alist-val
          • Not*
          • Free-list-of-fast-alists
          • *nls*
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Utilities

Vl-maybe-string-list

A list of maybe-stringp objects.

This is an ordinary fty::deflist.

Subtopics

Vl-maybe-string-list-fix
(vl-maybe-string-list-fix x) is a usual fty list fixing function.
Vl-maybe-string-list-equiv
Basic equivalence relation for vl-maybe-string-list structures.
Vl-maybe-string-list-p
(vl-maybe-string-list-p x) recognizes lists where every element satisfies maybe-stringp.