Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
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-plural-p
Vl-remove-keys
Vl-merge-contiguous-indices
Vl-edition-p
Sum-nats
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
True-list-listp
Symbol-list-listp
Explode-list
All-have-len
Pos-listp
Min-nats
Debuggable-and
Vl-starname
Remove-equal-without-guard
Vl-maybe-string-list
Vl-maybe-string-list-fix
Vl-maybe-string-list-equiv
Vl-maybe-string-list-p
String-fix
Longer-than-p
Anyp
Fast-alist-free-each-alist-val
Not*
Free-list-of-fast-alists
*nls*
Printer
Kit
Mlib
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
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
.