Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Hons-and-memoization
Events
History
Parallelism
Programming
Defun
Declare
Stobj
State
Memoize
Mbe
Io
Apply$
System-utilities
Defpkg
Mutual-recursion
Arrays
Programming-with-state
Characters
Loop$
Time$
Defmacro
Defconst
Guard
Evaluation
Equality-variants
Fast-alists
Compilation
Hons
ACL2-built-ins
Advanced-features
Set-check-invariant-risk
Developers-guide
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Defabbrev
Conses
Alists
Set-register-invariant-risk
Strings
Std/strings
String-listp
Stringp
Length
Search
Remove-duplicates
Position
Coerce
Concatenate
Reverse
String
Subseq
Substitute
Count
Char
String-downcase
String-upcase
String<
String-equal
String-utilities
String-append
String>=
String<=
String>
Hex-digit-char-theorems
String-downcase-gen
String-upcase-gen
Program-wrapper
Get-internal-time
Basics
Packages
System-attachments
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Defopen
Sleep
Real
ACL2-tutorial
Debugging
Miscellaneous
Prover-output
Built-in-theorems
Macros
Interfacing-tools
About-ACL2
Interfacing-tools
Hardware-verification
Software-verification
Testing-utilities
Math
Strings
ACL2-built-ins
Stringp
Recognizer for strings
(
stringp
x)
is true if and only if
x
is a string.