Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Xdoc
ACL2-doc
Recursion-and-induction
Loop$-primer
Operational-semantics
Pointers
Plist-worldp
Type
Community-book
Member-equal
Hons-member-equal
Event
Stobjs-out
Value
Stobj-let
Member-eq
Assoc-equal
Open-input-channel
Show-accumulated-persistence
Array
Multiple-value
Boolean-convention
Ignore
Declaration
Stobjs-in
Memoization
Cons-term
To-df
Set-ld-skip-proofsp
Redundant
Non-executable
Genvar
Fcons-term
Subsetp-equal
Open-output-channel
No-duplicatesp-equal
Function-symbolp
Fast-alist
Keyword
Iprinting
Formals
Expand
Default-verify-guards-eagerness
Close-output-channel
Trust-tag
Set-fast-cert
Read-object
Pe-table
Normalization
Meta-extract-global-fact
Df=
Dfp
Body
Inline
Table-alist
Sublis-var
Recursivep
Read-char$
Read-byte$
Raw-mode
Open-input-channel-p
Observation-cw
Fmt-to-string
Df-
Assoc-eq
All-vars
Add-suffix-to-fn
Add-suffix
Abstract-stobj
Package
Optimize
Ignorable
Waterfall
Untranslate-preprocess
Union-eq
Stobjs
Set-serialize-character
Remove-duplicates-equal
Position-equal
Mfc-rw
Iprint
Er-let*
Df+
Df-sin
Close-input-channel
All-fnnames1
Write-byte$
Use
Time-limit
Tamep
Subsetp-eq
Step-limit
Split-types
Restrict
Remove-equal
Quotep
Put-assoc-equal
Position-eq
Open-output-channel-p
No-duplicatesp-eq
Mfc-ts
Mfc-rw+
Mfc-ap
Ld-history-entry-error-flg
Intersectp-equal
Intersectp-eq
Induct
Get-check-invariant-risk
Fmt-soft-right-margin
Doublet-listp
Defpm
Binary-df+
All-fnnames
Adjust-ld-history
Accumulated-persistence-oops
Vl-packeddimension
Error
With-output!
When$
Unknown-constraints
Union-equal
Typespec-check
Translate
Trans-eval-default-warning
Tamep-lambdap
Tag-tree
Symbol-class
Sublis-fn-simple
Sublis-fn-lst-simple
Sublis-fn
Stable-under-simplificationp
Set-slow-alist-action
Set-ruler-extenders
Set-ld-skip-proofs
Set-ld-redefinition-action
Set-ld-prompt
Set-ld-pre-eval-print
Set-ld-keyword-aliases
Set-ld-always-skip-top-level-locals
Set-difference-eq
Reorder
Remove1-equal
Remove-eq
Remove-assoc-equal
Regression
Rassoc-equal
Rassoc-eq
Prettyify-clause
Peek-char$
Partition-rest-and-keyword-args
Mode
Mfc-world
Mfc-relieve-hyp
Mfc-rdepth
Mfc-ancestors
Mfc
Meta-extract-global-fact+
Meta-extract-formula
Meta-extract-contextual-fact
Maybe-convert-to-mv
Logicp
Legal-constantp
Ld-history-entry-user-data
Ld-history-entry-input
Intersection-eq
Guard-hints
Guard-checking
Get-skipped-proofs-p
Get-register-invariant-risk
Get-in-theory-redundant-okp
Fsubcor-var
From-df
Flatten-ands-in-lit
Ffn-symb
Fargs
Ev$-list
Er-let*-cmp
Enabled-runep
Enabled-numep
Dumb-occur-var
Dumb-negate-lit
Disjoin
Df/
Df<=
Df<
Df-pi
Df-log
Df-cosh-fn
Df-cos-fn
Df-abs-fn
Df-abs
Cw-gstack-for-subterm
Context
Cons-term*
Conjoin2
Conjoin
Cases
Backchain-limit-rw
Arglistp
Allow-real-oracle-eval
All-fnnames-lst
All-attachments
Add-to-set-eq
Add-ld-keyword-alias!
Add-ld-keyword-alias
Pbkdf2-hmac-sha-512
Double-float
Uses-cpp
Cert-flags
Show-simplify-term
Show-simplify-defun-sk
Show-simplify-defun
Weak-ld-history-entry-p
Verify-guards-eagerness
Variablep
Value-cmp
Undoing
Unary-df/
Unary-df-log
Unary-df-
Ttag
Trivial-ancestors-check
Translate-hints
Trans-eval-no-warning
Top-level-loop
Too-many-ifs
To-dfp
Tamep-functionp
Symbol-doublet-listp
Sum$+
Suitably-tamep-listp
Subst-var
Subst-expr
Subsequencep
Subcor-var
Stv
Stobjp
Set-trace-co
Set-standard-oi
Set-standard-co
Set-proofs-co
Set-non-linear
Set-let*-abstraction
Set-ld-verbose
Set-ld-user-stobjs-modified-warning
Set-ld-query-control-alist
Set-ld-pre-eval-filter
Set-ld-post-eval-print
Set-ld-missing-input-ok
Set-ld-keyword-aliases!
Set-ld-evisc-tuple
Set-ld-error-triples
Set-ld-error-action
Set-difference-equal
Set-accumulated-persistence
Saving-and-restoring
Rize
Rewrite-cache
Reset-print-control
Remove1-eq
Remove1-assoc-equal
Remove1-assoc-eq
Remove-duplicates-eq
Remove-assoc-eq
Put-assoc-eq
Proof-supporters-alist
Programp
Print-object$-preserving-case
Nvariablep
Nonlinearp
No-thanks
No-op
Mfc-unify-subst
Mfc-type-alist
Mfc-clause
Match-free
Make-lambda-term
Make-lambda-application
Make-lambda
Lisp-programmer-introduction
Let-mbe
Legal-variablep
Ld-user-stobjs-modified-warning
Ld-history-entry-value
Ld-history-entry-stobjs-out/value
Ld-history-entry-stobjs-out
Lambda-formals
Lambda-body
Lambda-applicationp
Known-package-alist
Io?
Intersection-equal
Implicate
If-intro
Hands-off
Guards
Guard-holder
Get-serialize-character
Get-output-stream-string$
Get-event
Get-defun-event
Get-brr-local
Gcs
Fquotep
Fncall-term
Fn-symb
Fn-rune-nume
Fn-check-def
Fmx!-cw
Fmt-hard-right-margin
Flambdap
Flambda-applicationp
Fix-pkg
Ffnnamep-lst
Ffnnamep
Ffn-symb-p
Fdefun-mode
Fcons-term*
Fargn
Fake-rune
Er-progn-cmp
Er-cmp
Dumb-occur
Do-not-induct
Disjoin2
Df*
Df1
Df0
Df-tanh-fn
Df-tan-fn
Df-string
Df-sqrt-fn
Df-sinh-fn
Df-sin-fn
Df-round
Df-minus-1
Df-expt-fn
Df-exp-fn
Df-atanh-fn
Df-atan-fn
Df-asinh-fn
Df-asin-fn
Df-acosh-fn
Df-acos-fn
Defined-constant
Default-state-vars
Computed-hint
Collect$+
Collect$
Check-invariant-risk
Ccl-updates
By
Binary-df/
Binary-df*
Binary-df-log
Backtrack
Always$+
All-calls
Add-to-set-equal
Add-to-set-eql
ACL2s
ACL2-unwind-protect
Syntax
Build-the-manual
Sha-512
Sha-384
Sha-256
Sha-224
Pad-to-896
Pad-to-448
Mimcsponge-semaphore
Mimcsponge
Keccak-512-bytes
Keccak-512
Keccak-384-bytes
Keccak-384
Keccak-256-bytes
Keccak-256
Keccak-224-bytes
Keccak-224
Pbkdf2-hmac-sha-512-from-strings
Hmac-sha-512
Hmac-sha-256
&whole
&rest
&optional
&key
&body
&allow-other-keys
Apropos
Uses-stp
Uses-smtlink
Uses-quicklisp
Uses-ipasir
Uses-glucose
Uses-ACL2r
Uses-abc
Reloc-stub
Pcert
Non-sbcl
Non-lispworks
Non-gcl
Non-cmucl
Non-allegro
Non-ACL2r
Non-ACL2p
Ccl-only
Ansi-only
ACL2xskip
ACL2x
Show-simplify-defun+
*df-pi*
Wormhole-coherence
With-prover-step-limit!
When$+
Untouchable-marker
Until$+
Until$
Translate11
Translate1-cmp
Translate1
Translate-cmp
Thereis$+
Thereis$
Sum$
Single-threaded-objects
Set-theory
Set-temp-touchable-vars
Set-temp-touchable-fns
Set-print-right-margin
Set-print-readably
Set-print-lines
Set-print-level
Set-print-length
Set-print-escape
Set-print-circle
Rw-cache
Runes-diff
Ruler
Remove-guard-holders
Redefining
Redefine
Read-object-with-case
Read-object-suppress
Put-assoc-eql
Print-summary-user
Pound-u-reader
Pound-dot-reader
Pound-bang-reader
Plev-min
Plev-mid
Plev-max
Plev-info
Persistent-whs
Old-and-new-event-data
Note9
Note8-update
Note8
Note7
Note6
Note5
Note4
Note3
Note2
Note1
Nfix-list
Meta-extract-rw+-term
Memoize-prover-fns
Measure-theorem
Make-list-ac
Loop$-for
Loop$-do
Lexp
Lex-fix
Interrupts
Install-skip-in-book
Immed-forced
Ilks
Hash-tables
Guard-msg-table
Getting-started
Forced
Fmt!-to-string
Fmt1!-to-string
Fmt1-to-string
Fms!-to-string
Fms-to-string
Floating-point
First-n-ac
First-keyword
Fast-alist-discipline
External-format
Extended-syntaxp
Execution
Event-data
Ephemeral-whs
D<
Dynamically-monitor-rewrites
Df/=-fn
Df>=
Df>
Df=-fn
Df<-fn
Df-tanh
Df-tan
Df-sqrt
Df-sinh
Df-rationalize
Df-expt
Df-exp
Df-cosh
Df-cos
Df-atanh
Df-atan
Df-asinh
Df-asin
Df-acosh
Df-acos
Defthmdr
Cw-gstack-for-term*
Cw-gstack-for-term
Cw-gstack-for-subterm*
ACL2::counter-example-generation
Comma-atsign
Comma
Coherence
Check-sum
Certifying-books
Certify-book-failure
Book-makefiles
Auto-termination
Auto-instance
Assocs
Assertions
Append$+
Append$
Always$
ACL2r
ACL2p
Doc
Documentation-copyright
Course-materials
Args
ACL2-doc-summary
Finding-documentation
Broken-link
Doc-terminal-test-2
Doc-terminal-test-1
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Pointers
Member-equal
See
member
.
Subtopics
Hons-member-equal
MEMBER-EQUAL using HONS-EQUAL for each equality check
