		Search-engine friendly clone of the ACL2 documentation.

ACL2

Miscellaneous

A miscellany of documented functions and concepts (often cited in more accessible documentation)

Perhaps as the system matures this section will become more structured.

Subtopics

Term: The three senses of well-formed ACL2 expressions or formulas
Ld: The ACL2 read-eval-print loop, file loader, and command processor
Hints: Advice to the theorem proving process
Type-set: How type information is encoded in ACL2
Ordinals: Ordinals in ACL2
Clause: A representation of prover goals
ACL2-customization: File of initial commands for ACL2 to run at startup
With-prover-step-limit: Limit the number of steps for proofs
Set-prover-step-limit: Sets the step-limit used by the ACL2 prover
With-prover-time-limit: Limit the time for proofs
Local-incompatibility: When non-local events won't replay in isolation
Set-case-split-limitations: Set the case-split-limitations
Subversive-recursions: Why we restrict encapsulated recursive functions
Specious-simplification: Nonproductive proof steps
Defsum: Define a recursive data type similar to a Haskell type definition.
Gcl: Tips on building and using ACL2 based on Gnu Common Lisp
Oracle-timelimit: Carry out some computation, returning (not just printing!) how long it took and (on supported Lisps) how many bytes were allocated, but aborting the execution if it takes too long.
Thm: Prove a theorem
Defopener: Create a defthm equating a call with its simplification.
Case-split-limitations: Limiting the number of immediate subgoals
Set-gc-strategy: Set the garbage collection strategy (CCL only)
Default-defun-mode: The default defun-mode of defun'd functions
Top-level: Evaluate a top-level form as a function body
Reader: Reading expressions in the ACL2 read-eval-print loop
Ttags-seen: List some declared trust tags (ttags)
Adviser: A extensible hint suggestion daemon
Ttree: Tag-trees
Abort-soft: Control how interrupts are handled in proofs
Defsums: Define a set of mutually-recursive data types.
Gc$: Invoke the garbage collector
With-timeout: Evaluate form with a timeout (in seconds)
Coi-debug::fail: A macro to assist in signalling runtime errors
Expander: Routines for simplifying terms.
Gc-strategy: The garbage collection strategy
Coi-debug::assert: A macro to assist in detecting runtime errors
Sin-cos: SIN/COS approximations.
Def::doc: A simple macro for easing the documentation process
Syntax: The syntax of ACL2 is that of Common Lisp
Subversive-inductions: Why we restrict encapsulated recursive functions