		Search-engine friendly clone of the ACL2 documentation.

Documentation

Pointers

Links pointing to relevant documentation topics

Subtopics

Plist-worldp: See system-utilities.
Type: Disambiguation page for type-related concepts.
Community-book: See community-books.
Member-equal: See member.
Event: See events.
Stobjs-out: See system-utilities.
Stobj-let: See nested-stobjs.
Member-eq: See member.
Value: See system-utilities.
Assoc-equal: See assoc.
Open-input-channel: See io.
Show-accumulated-persistence: See accumulated-persistence.
Array: See arrays.
Multiple-value: See mv-let.
Boolean-convention: See 4vec-operations.
Ignore: See declare.
Declaration: See declare.
Stobjs-in: See system-utilities.
Memoization: See memoize.
Cons-term: See system-utilities.
To-df: See df.
Set-ld-skip-proofsp: See ld-skip-proofsp.
Redundant: See redundant-events.
Non-executable: See xargs for information about the keyword :non-executable.
Genvar: See system-utilities.
Fcons-term: See system-utilities.
Subsetp-equal: See subsetp.
Open-output-channel: See io.
No-duplicatesp-equal: See no-duplicatesp.
Function-symbolp: See system-utilities.
Fast-alist: See fast-alists.
Keyword: See keywordp.
Iprinting: See set-iprint.
Formals: See system-utilities.
Expand: See hints for information about the keyword :expand.
Default-verify-guards-eagerness: See set-verify-guards-eagerness.
Close-output-channel: See io.
Trust-tag: See defttag.
Set-fast-cert: See fast-cert.
Read-object: See io.
Pe-table: See extend-pe-table.
Normalization: See normalize.
Meta-extract-global-fact: See meta-extract.
Df=: See df.
Dfp: See df.
Body: See system-utilities.
Inline: See defun-inline.
Table-alist: See table.
Sublis-var: See system-utilities.
Recursivep: See system-utilities.
Read-char$: See io.
Read-byte$: See io.
Observation-cw: See observation.
Fmt-to-string: See printing-to-strings.
Df-: See df.
Assoc-eq: See assoc.
All-vars: See system-utilities.
Add-suffix-to-fn: See system-utilities.
Add-suffix: See system-utilities.
Abstract-stobj: See defabsstobj.
Optimize: See declare.
Ignorable: See declare.
Waterfall: See hints-and-the-waterfall.
Untranslate-preprocess: See user-defined-functions-table.
Union-eq: See union$.
Stobjs: See xargs for information about the keyword :stobjs.
Set-serialize-character: See with-serialize-character.
Remove-duplicates-equal: See remove-duplicates.
Raw-mode: See set-raw-mode.
Position-equal: See position.
Open-input-channel-p: See io.
Mfc-rw: See extended-metafunctions.
Iprint: See set-iprint.
Er-let*: See programming-with-state.
Df+: See df.
Df-sin: See df.
Close-input-channel: See io.
All-fnnames1: See system-utilities.
Package: See packages.
Write-byte$: See io.
Use: See hints for information about the keyword :use.
Time-limit: See with-prover-time-limit.
Tamep: See tame.
Subsetp-eq: See subsetp.
Step-limit: See with-prover-step-limit.
Split-types: See xargs for information about the keyword :split-types.
Restrict: See hints for information about the keyword :restrict.
Remove-equal: See remove.
Quotep: See system-utilities.
Put-assoc-equal: See put-assoc.
Position-eq: See position.
Open-output-channel-p: See io.
No-duplicatesp-eq: See no-duplicatesp.
Mfc-ts: See extended-metafunctions.
Mfc-rw+: See extended-metafunctions.
Mfc-ap: See extended-metafunctions.
Ld-history-entry-error-flg: See ld-history.
Intersectp-equal: See intersectp.
Intersectp-eq: See intersectp.
Induct: See hints for information about the keyword :induct.
Get-check-invariant-risk: See set-check-invariant-risk.
Fmt-soft-right-margin: See set-fmt-hard-right-margin.
Doublet-listp: See system-utilities.
Defpm: See def-partial-measure.
Binary-df+: See df.
All-fnnames: See system-utilities.
Adjust-ld-history: See ld-history.
Accumulated-persistence-oops: See accumulated-persistence.
Vl-packeddimension: See vl-packeddimension-p.
Error: See hints for information about the keyword :error.
With-output!: See with-output.
When$: See loop$.
Unknown-constraints: See partial-encapsulate.
Union-equal: See union$.
Typespec-check: See meta-extract.
Translate: See system-utilities.
Trans-eval-default-warning: See user-stobjs-modified-warnings.
Tamep-lambdap: See tame.
Tag-tree: See ttree.
Symbol-class: See system-utilities.
Sublis-fn-simple: See system-utilities.
Sublis-fn-lst-simple: See system-utilities.
Sublis-fn: See system-utilities.
Stable-under-simplificationp: See computed-hints.
Set-slow-alist-action: See slow-alist-warning.
Set-ruler-extenders: See rulers.
Set-ld-skip-proofs: See ld-skip-proofsp.
Set-ld-redefinition-action: See ld-redefinition-action.
Set-ld-prompt: See ld-prompt.
Set-ld-pre-eval-print: See ld-pre-eval-print.
Set-ld-keyword-aliases: See ld-keyword-aliases.
Set-ld-always-skip-top-level-locals: See ld-always-skip-top-level-locals.
Set-difference-eq: See set-difference$.
Reorder: See hints for information about the keyword :reorder.
Remove1-equal: See remove1.
Remove-eq: See remove.
Remove-assoc-equal: See remove-assoc.
Regression: See books-certification.
Rassoc-equal: See rassoc.
Rassoc-eq: See rassoc.
Prettyify-clause: See system-utilities.
Peek-char$: See io.
Partition-rest-and-keyword-args: See system-utilities.
Mode: See xargs for information about the keyword :mode.
Mfc-world: See extended-metafunctions.
Mfc-relieve-hyp: See extended-metafunctions.
Mfc-rdepth: See extended-metafunctions.
Mfc-ancestors: See extended-metafunctions.
Mfc: See metafunction-context.
Meta-extract-global-fact+: See meta-extract.
Meta-extract-formula: See meta-extract.
Meta-extract-contextual-fact: See meta-extract.
Maybe-convert-to-mv: See system-utilities.
Logicp: See system-utilities.
Legal-constantp: See system-utilities.
Ld-history-entry-user-data: See ld-history.
Ld-history-entry-input: See ld-history.
Intersection-eq: See intersection$.
Guard-hints: See xargs for information about the keyword :guard-hints.
Guard-checking: See set-guard-checking.
Get-skipped-proofs-p: See system-utilities.
Get-register-invariant-risk: See set-register-invariant-risk.
Get-in-theory-redundant-okp: See set-in-theory-redundant-okp.
Fsubcor-var: See system-utilities.
From-df: See df.
Flatten-ands-in-lit: See system-utilities.
Ffn-symb: See system-utilities.
Fargs: See system-utilities.
Ev$-list: See apply$.
Er-let*-cmp: See context-message-pair.
Enabled-runep: See system-utilities.
Enabled-numep: See system-utilities.
Dumb-occur-var: See system-utilities.
Dumb-negate-lit: See system-utilities.
Disjoin: See system-utilities.
Df/: See df.
Df<=: See df.
Df<: See df.
Df-pi: See df.
Df-log: See df.
Df-cosh-fn: See df.
Df-cos-fn: See df.
Df-abs-fn: See df.
Df-abs: See df.
Cw-gstack-for-subterm: See with-brr-data.
Context: See ctx.
Cons-term*: See system-utilities.
Conjoin2: See system-utilities.
Conjoin: See system-utilities.
Cases: See hints for information about the keyword :cases.
Backchain-limit-rw: See hints for information about the keyword :backchain-limit-rw.
Arglistp: See system-utilities.
Allow-real-oracle-eval: See oracle-eval.
All-fnnames-lst: See system-utilities.
All-attachments: See system-utilities.
Add-to-set-eq: See add-to-set.
Add-ld-keyword-alias!: See ld-keyword-aliases.
Add-ld-keyword-alias: See ld-keyword-aliases.
Pbkdf2-hmac-sha-512: See kdf.
Double-float: See df.
Uses-cpp: See cert_param.
Cert-flags: See custom-certify-book-commands.
Show-simplify-term: See simplify-term.
Show-simplify-defun-sk: See simplify-defun-sk.
Show-simplify-defun: See simplify-defun.
Weak-ld-history-entry-p: See ld-history.
Verify-guards-eagerness: See set-verify-guards-eagerness.
Variablep: See system-utilities.
Value-cmp: See context-message-pair.
Undoing: See undo.
Unary-df/: See df.
Unary-df-log: See df.
Unary-df-: See df.
Ttag: See defttag.
Trivial-ancestors-check: See use-trivial-ancestors-check.
Translate-hints: See system-utilities.
Trans-eval-no-warning: See user-stobjs-modified-warnings.
Top-level-loop: See guarantees-of-the-top-level-loop.
Too-many-ifs: See efficiency.
To-dfp: See df.
Tamep-functionp: See tame.
Symbol-doublet-listp: See system-utilities.
Sum$+: See loop$.
Suitably-tamep-listp: See tame.
Subst-var: See system-utilities.
Subst-expr: See system-utilities.
Subsequencep: See system-utilities.
Subcor-var: See system-utilities.
Stv: See symbolic-test-vectors.
Stobjp: See system-utilities.
Set-trace-co: See trace-co.
Set-standard-oi: See standard-oi.
Set-standard-co: See standard-co.
Set-proofs-co: See proofs-co.
Set-non-linear: See set-non-linearp.
Set-let*-abstraction: See set-let*-abstractionp.
Set-ld-verbose: See ld-verbose.
Set-ld-user-stobjs-modified-warning: See user-stobjs-modified-warnings.
Set-ld-query-control-alist: See ld-query-control-alist.
Set-ld-pre-eval-filter: See ld-pre-eval-filter.
Set-ld-post-eval-print: See ld-post-eval-print.
Set-ld-missing-input-ok: See ld-missing-input-ok.
Set-ld-keyword-aliases!: See ld-keyword-aliases.
Set-ld-evisc-tuple: See ld-evisc-tuple.
Set-ld-error-triples: See ld-error-triples.
Set-ld-error-action: See ld-error-action.
Set-difference-equal: See set-difference$.
Set-accumulated-persistence: See accumulated-persistence.
Saving-and-restoring: See save-exec.
Rize: See df.
Rewrite-cache: See set-rw-cache-state.
Reset-print-control: See print-control.
Remove1-eq: See remove1.
Remove1-assoc-equal: See remove1-assoc.
Remove1-assoc-eq: See remove1-assoc.
Remove-duplicates-eq: See remove-duplicates.
Remove-assoc-eq: See remove-assoc.
Put-assoc-eq: See put-assoc.
Proof-supporters-alist: See dead-events.
Programp: See system-utilities.
Print-object$-preserving-case: See io.
Nvariablep: See system-utilities.
Nonlinearp: See hints for information about the keyword :nonlinearp.
No-thanks: See hints for information about the keyword :no-thanks.
No-op: See hints for information about the keyword :no-op.
Mfc-unify-subst: See extended-metafunctions.
Mfc-type-alist: See extended-metafunctions.
Mfc-clause: See extended-metafunctions.
Match-free: See free-variables.
Make-lambda-term: See system-utilities.
Make-lambda-application: See system-utilities.
Make-lambda: See system-utilities.
Lisp-programmer-introduction: See introduction-to-programming-in-ACL2-for-those-who-know-lisp.
Let-mbe: See equality-variants-details.
Legal-variablep: See system-utilities.
Ld-user-stobjs-modified-warning: See user-stobjs-modified-warnings.
Ld-history-entry-value: See ld-history.
Ld-history-entry-stobjs-out/value: See ld-history.
Ld-history-entry-stobjs-out: See ld-history.
Lambda-formals: See system-utilities.
Lambda-body: See system-utilities.
Lambda-applicationp: See system-utilities.
Known-package-alist: See system-utilities.
Io?: See system-utilities.
Intersection-equal: See intersection$.
Implicate: See system-utilities.
If-intro: See splitter.
Hands-off: See hints for information about the keyword :hands-off.
Guards: See guard.
Guard-holder: See guard-holders.
Get-serialize-character: See with-serialize-character.
Get-output-stream-string$: See io.
Get-event: See system-utilities.
Get-defun-event: See system-utilities.
Get-brr-local: See system-utilities.
Gcs: See get-command-sequence.
Fquotep: See system-utilities.
Fncall-term: See meta-extract.
Fn-symb: See system-utilities.
Fn-rune-nume: See system-utilities.
Fn-check-def: See fn-get-def.
Fmx!-cw: See fmx-cw.
Fmt-hard-right-margin: See set-fmt-hard-right-margin.
Flambdap: See system-utilities.
Flambda-applicationp: See system-utilities.
Fix-pkg: See system-utilities.
Ffnnamep-lst: See system-utilities.
Ffnnamep: See system-utilities.
Ffn-symb-p: See system-utilities.
Fdefun-mode: See system-utilities.
Fcons-term*: See system-utilities.
Fargn: See system-utilities.
Fake-rune: See rune.
Er-progn-cmp: See context-message-pair.
Er-cmp: See context-message-pair.
Dumb-occur: See system-utilities.
Do-not-induct: See hints for information about the keyword :do-not-induct.
Disjoin2: See system-utilities.
Df*: See df.
Df1: See df.
Df0: See df.
Df-tanh-fn: See df.
Df-tan-fn: See df.
Df-string: See df.
Df-sqrt-fn: See df.
Df-sinh-fn: See df.
Df-sin-fn: See df.
Df-round: See df.
Df-minus-1: See df.
Df-expt-fn: See df.
Df-exp-fn: See df.
Df-atanh-fn: See df.
Df-atan-fn: See df.
Df-asinh-fn: See df.
Df-asin-fn: See df.
Df-acosh-fn: See df.
Df-acos-fn: See df.
Defined-constant: See system-utilities.
Default-state-vars: See system-utilities.
Computed-hint: See computed-hints.
Collect$+: See loop$.
Collect$: See loop$.
Check-invariant-risk: See set-check-invariant-risk.
Ccl-updates: See ccl-installation.
By: See hints for information about the keyword :by.
Binary-df/: See df.
Binary-df*: See df.
Binary-df-log: See df.
Backtrack: See hints for information about the keyword :backtrack.
Always$+: See loop$.
All-calls: See system-utilities.
Add-to-set-equal: See add-to-set.
Add-to-set-eql: See add-to-set.
ACL2s: See ACL2-sedan.
ACL2-unwind-protect: See system-utilities.
Syntax: See markup.
Build-the-manual: See xdoc.
Sha-512: See sha-2.
Sha-384: See sha-2.
Sha-256: See sha-2.
Sha-224: See sha-2.
Pad-to-896: See padding.
Pad-to-448: See padding.
Mimcsponge-semaphore: See mimc.
Mimcsponge: See mimc.
Keccak-512-bytes: See keccak.
Keccak-512: See keccak.
Keccak-384-bytes: See keccak.
Keccak-384: See keccak.
Keccak-256-bytes: See keccak.
Keccak-256: See keccak.
Keccak-224-bytes: See keccak.
Keccak-224: See keccak.
Pbkdf2-hmac-sha-512-from-strings: See kdf.
Hmac-sha-512: See hmac.
Hmac-sha-256: See hmac.
&whole: See macro-args.
&rest: See macro-args.
&optional: See macro-args.
&key: See macro-args.
&body: See macro-args.
&allow-other-keys: See macro-args.
Apropos: See finding-documentation.
Uses-stp: See cert_param.
Uses-smtlink: See cert_param.
Uses-quicklisp: See cert_param.
Uses-ipasir: See cert_param.
Uses-glucose: See cert_param.
Uses-ACL2r: See cert_param.
Uses-abc: See cert_param.
Reloc-stub: See cert_param.
Pcert: See cert_param.
Non-sbcl: See cert_param.
Non-lispworks: See cert_param.
Non-gcl: See cert_param.
Non-cmucl: See cert_param.
Non-allegro: See cert_param.
Non-ACL2r: See cert_param.
Non-ACL2p: See cert_param.
Ccl-only: See cert_param.
Ansi-only: See cert_param.
ACL2xskip: See cert_param.
ACL2x: See cert_param.
Show-simplify-defun+: See simplify-defun+.
*df-pi*: See df.
Wormhole-coherence: See wormhole-status.
With-prover-step-limit!: See with-prover-step-limit.
When$+: See loop$.
Untouchable-marker: See defmacro-untouchable.
Until$+: See loop$.
Until$: See loop$.
Translate11: See system-utilities.
Translate1-cmp: See system-utilities.
Translate1: See system-utilities.
Translate-cmp: See system-utilities.
Thereis$+: See loop$.
Thereis$: See loop$.
Sum$: See loop$.
Single-threaded-objects: See stobj.
Set-temp-touchable-vars: See remove-untouchable.
Set-temp-touchable-fns: See remove-untouchable.
Set-print-right-margin: See print-control.
Set-print-readably: See print-control.
Set-print-lines: See print-control.
Set-print-level: See print-control.
Set-print-length: See print-control.
Set-print-escape: See print-control.
Set-print-circle: See print-control.
Rw-cache: See set-rw-cache-state.
Runes-diff: See saving-event-data.
Ruler: See rulers.
Remove-guard-holders: See guard-holders.
Redefining: See ld-redefinition-action.
Redefine: See ld-redefinition-action.
Read-object-with-case: See io.
Read-object-suppress: See io.
Put-assoc-eql: See put-assoc.
Print-summary-user: See finalize-event-user.
Pound-u-reader: See sharp-u-reader.
Pound-dot-reader: See sharp-dot-reader.
Pound-bang-reader: See sharp-bang-reader.
Plev-min: See plev.
Plev-mid: See plev.
Plev-max: See plev.
Plev-info: See plev.
Persistent-whs: See wormhole-status.
Old-and-new-event-data: See saving-event-data.
Note9: See note-1-9.
Note8-update: See note-1-8-update.
Note8: See note-1-8.
Note7: See note-1-7.
Note6: See note-1-6.
Note5: See note-1-5.
Note4: See note-1-4.
Note3: See note-1-3.
Note2: See note-1-2.
Note1: See note-1-1.
Nfix-list: See l<.
Meta-extract-rw+-term: See meta-extract.
Memoize-prover-fns: See memoized-prover-fns.
Measure-theorem: See termination-theorem.
Make-list-ac: See make-list.
Loop$-for: See for-loop$.
Loop$-do: See do-loop$.
Lexp: See l<.
Lex-fix: See l<.
Interrupts: See abort-soft.
Install-skip-in-book: See skip-in-book.
Immed-forced: See splitter.
Ilks: See ilk.
Hash-tables: See defstobj.
Guard-msg-table: See set-guard-msg.
Getting-started: See ACL2-tutorial.
Forced: See force.
Fmt!-to-string: See printing-to-strings.
Fmt1!-to-string: See printing-to-strings.
Fmt1-to-string: See printing-to-strings.
Fms!-to-string: See printing-to-strings.
Fms-to-string: See printing-to-strings.
Floating-point: See df.
First-n-ac: See take.
First-keyword: See system-utilities.
Fast-alist-discipline: See slow-alist-warning.
External-format: See character-encoding.
Extended-syntaxp: See syntaxp.
Execution: See evaluation.
Event-data: See saving-event-data.
Ephemeral-whs: See wormhole-status.
D<: See l<.
Dynamically-monitor-rewrites: See dmr.
Df/=-fn: See df.
Df>=: See df.
Df>: See df.
Df=-fn: See df.
Df<-fn: See df.
Df-tanh: See df.
Df-tan: See df.
Df-sqrt: See df.
Df-sinh: See df.
Df-rationalize: See df.
Df-expt: See df.
Df-exp: See df.
Df-cosh: See df.
Df-cos: See df.
Df-atanh: See df.
Df-atan: See df.
Df-asinh: See df.
Df-asin: See df.
Df-acosh: See df.
Df-acos: See df.
Defthmdr: See defthmr.
Cw-gstack-for-term*: See with-brr-data.
Cw-gstack-for-term: See with-brr-data.
Cw-gstack-for-subterm*: See with-brr-data.
ACL2::counter-example-generation: See cgen.
Comma-atsign: See backquote.
Comma: See backquote.
Coherence: See wormhole-status.
Check-sum: See checksum.
Certifying-books: See books-certification.
Certify-book-failure: See certify-book-debug.
Book-makefiles: See books-certification.
Auto-termination: See defunt.
Auto-instance: See defthm<w.
Assocs: See patbind-assocs.
Assertions: See errors.
Append$+: See loop$.
Append$: See loop$.
Always$: See loop$.
ACL2r: See real.
ACL2p: See parallelism.