Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Defun
Declare
System-utilities
Stobj
State
Mutual-recursion
Memoize
Mbe
Io
Defpkg
Apply$
Loop$
Programming-with-state
Arrays
Characters
Time$
Loop$-primer
Fast-alists
Defconst
Defmacro
Evaluation
Guard
Equality-variants
Compilation
Hons
ACL2-built-ins
Let
Declare
Mbe
Apply$
Fmt
Loop$
Return-last
Mv-let
Df
Pseudo-termp
Defwarrant
Time$
Mbt
Ec-call
Mv-nth
Sys-call
Msg
Er
Value-triple
Comp
O-p
Member
O<
Cw
Flet
Cbd
Or
Hons
Mv
Defbadge
Append
*ACL2-exports*
Eql
Comment
Unsigned-byte-p
Posp
Natp
The
Nth
And
Len
List
Time-tracker
Term-order
True-listp
Msgp
Booleanp
<
If
Pseudo-term-listp
+
Not
With-global-stobj
Bitp
Equal
Cdr
Car
String-listp
Nat-listp
Implies
Iff
Character-listp
Alistp
Cons
Symbol-listp
Quote
Integerp
Consp
True-list-listp
State-global-let*
Compress1
Symbolp
Stringp
Macrolet
*common-lisp-symbols-from-main-lisp-package*
Characterp
Prog2$
*
Last-prover-steps
Hons-acons
Eq
Let*
@
With-guard-checking
With-local-stobj
Length
Hard-error
-
Zp
Search
Intersection$
Assign
Aset1
Symbol-name
Union$
Set-gc-strategy
In-tau-intervalp
Break-on-error
Pand
Cons-with-hint
Case-match
Fast-alist-fork
Sys-call+
ACL2-count
Remove-duplicates
Signed-byte-p
With-serialize-character
Observation
Hons-resize
Make-tau-interval
Logbitp
Termp
Position
Assoc
*standard-co*
Hons-acons!
Aref1
Read-run-time
Update-nth
Take
Hons-wash
Symbol-package-name
Expt
Coerce
Keywordp
Intern
Non-exec
Case
Standard-oi
Standard-co
Get-internal-time
Formula
Atom
Without-evisc
Good-bye
With-local-state
Spec-mv-let
Intern-in-package-of-symbol
Hons-clear
Binary-+
Ash
With-fast-alist
Symbol-alistp
Set-difference$
Flush-compress
Rationalp
Por
<=
Rassoc
Remove-assoc
=
Nthcdr
Pargs
Nfix
Hons-copy
Alphorder
Subsetp
Logand
Remove1-assoc
No-duplicatesp
Mv-list
Canonical-pathname
Aset2
Floor
Serialize-read
Random$
Fmt-to-comment-window
F-put-global
Compress2
Concatenate
Fast-alist-clean
Assert$
Remove
Remove1
Intersectp
Endp
Put-assoc
Princ$
Primitive
Keyword-value-listp
True-list-fix
Swap-stobjs
Illegal
Hons-get
With-output-lock
Setenv$
Open-output-channel!
Fast-alist-free
Er-progn
Cw-print-base-radix
Reverse
Cond
Complex
Add-to-set
Truncate
Digit-char-p
Code-char
Set-print-case
Set-print-base
Read-ACL2-oracle
Error1
Print-object$
Plet
Fmx-cw
Integer-length
Zip
With-live-state
Hons-assoc-equal
Extend-pathname
Logior
Char-code
With-guard-checking-event
Term-listp
Print-object$+
String
Mod
In-package
Unary--
Set-print-radix
Resize-list
Pkg-witness
Integer-listp
Revappend
Null
Term-list-listp
Make-fast-alist
Header
Boole$
Subseq
With-guard-checking-error-triple
/
Make-list
Logxor
Char-upcase
Char-downcase
Strip-cars
Set-fmt-hard-right-margin
Make-ord
Ifix
Fast-alist-free-on-exit
F-get-global
Aref2
Standard-char-p
Lognot
Must-be-equal
Integer-range-p
Getenv$
Binary-append
Er-hard
Eqlablep
Cpu-core-count
ACL2-numberp
Butlast
Pairlis$
Mod-expt
Hons-equal
Gc$
Boolean-listp
Substitute
Ceiling
With-stolen-alist
Mv?-let
String-upcase
String-downcase
Round
Count
Char
Sys-call-status
Progn$
Pprogn
Lexorder
Hons-summary
Break$
Assert*
Alpha-char-p
Strip-cdrs
Serialize-write
Keyword-listp
Logeqv
List*
Proofs-co
Maximum-length
Fix
Explode-nonnegative-integer
Eqlable-listp
Dimensions
Default
Arity
Upper-case-p
Sublis
Max
Lower-case-p
Evenp
Explode-atom
Change
Zerop
String<
String-equal
Last
Abs
Set-print-base-radix
Print-base-p
Nonnegative-integer-quotient
Intern$
Getprop
Binary-*
Aset1-trusted
Symbol<
String-append
Rfix
Mv?
Logic-fns-list-listp
Fast-alist-fork!
Er-hard?
Allocate-fixnum-range
Char-equal
1+
*standard-oi*
Sys-call*
Pos-listp
Mbt*
Hons-wash!
Hons-clear!
Signum
Rem
Real/rationalp
Rational-listp
O-first-coeff
Logic-fnsp
Logic-fns-listp
Hons-copy-persistent
Gc-strategy
Fast-alist-summary
String>=
String<=
Acons
O-first-expt
Fast-alist-clean!
>=
>
Subst
Logcount
Getpropc
Evens
Er-soft
Digit-to-char
Comp-gcl
Atom-listp
Arities-okp
ACL2-number-listp
/=
Cadr
*standard-ci*
Unary-/
The-true-list
Realfix
O-rst
Fast-alist-len
Complex/complex-rationalp
Array2p
Array1p
Logtest
Logandc1
Char<
Trace-co
Putprop
Get-real-time
Eqlable-alistp
Count-keys
Assoc-string-equal
Logorc1
Logandc2
1-
Packn
Logic-termp
Logic-term-list-listp
Fmt!
Fms
Cw!
Assoc-keyword
String>
Numerator
Logorc2
Denominator
Char>=
The-number
Odds
Makunbound-global
Make-character-list
Make
Get-cpu-time
Fmt-to-comment-window!
Fms!
F-boundp-global
Complex-rationalp
Alist-to-doublets
Access
Min
Lognor
Listp
Identity
Char>
Char<=
Zpf
Update-nth-array
Standard-char-listp
O-finp
Number-subtrees
Logic-term-listp
Last-cdr
Fmt1!
Fmt-to-comment-window!+
Character-alistp
Oddp
Minusp
Lognand
Imagpart
Conjugate
Xor
Unquote
String-alistp
Packn-pos
Maybe-flush-and-compress1
Kwote
Int=
Fmt1
Fmt-to-comment-window+
Cw-print-base-radix!
Alist-keys-subsetp
Realpart
Plusp
First
Symbol-name-lst
R-symbol-alistp
R-eqlable-alistp
Fmx
Cw!+
Cons-subtrees
Cons-count-bounded
Cddr
Caar
Proper-consp
Kwote-lst
Improper-consp
Cw+
Rest
Standard-char-p+
Mbe1
Caddr
Pairlis-x2
Pairlis-x1
O>=
O<=
O-infp
Merge-sort-lexorder
Fix-true-list
Cdddr
Set-fmt-soft-right-margin
Real-listp
O>
Cddar
Cdar
Cdadr
Cdaar
Cadar
Caadr
Caaar
Cadddr
Caddar
Third
Tenth
Sixth
Seventh
Second
Ninth
Fourth
Fifth
Eighth
Cddddr
Cdddar
Cddadr
Cddaar
Cdaddr
Cdadar
Cdaadr
Cdaaar
Cadadr
Cadaar
Caaddr
Caadar
Caaadr
Caaaar
Hons-shrink-alist!
Hons-shrink-alist
Flush-hons-get-hash-table-link
Delete-assoc
Developers-guide
System-attachments
Advanced-features
Set-check-invariant-risk
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
Program-wrapper
Get-internal-time
Basics
Packages
Oracle-eval
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Fake-oracle-eval
Defopen
Sleep
Operational-semantics
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Conses
ACL2-built-ins
Cddddr
cdr
of the
cdddr
See any Common Lisp documentation for details.