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

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

- 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
- ACL2-customization
- File of initial commands for ACL2 to run at startup
- With-prover-step-limit
- Limit the number of steps for proofs
- With-prover-time-limit
- Limit the time for proofs
- Set-prover-step-limit
- Sets the step-limit used by the ACL2 prover
- Set-case-split-limitations
- Set the case-split-limitations
- Subversive-recursions
- Why we restrict encapsulated recursive functions
- Local-incompatibility
- When non-local events won't replay in isolation
- Specious-simplification
- Nonproductive proof steps
- Defsum
- Define a recursive data type similar to a Haskell type definition.
- 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.
- Defopener
- Create a defthm equating a call with its simplification.
- Thm
- Prove a theorem
- Case-split-limitations
- Limiting the number of immediate subgoals
- Set-gc-strategy
- Set the garbage collection strategy (CCL only)
- Gcl
- Tips on building and using ACL2 based on Gnu Common Lisp
- 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