Functions that extend the logic

Any extension of the syntax of ACL2 (i.e., the definition of a new
constant or macro), the axioms (i.e., the definition of a function), or the
rule database (i.e., the proof of a theorem), constitutes a logical ``event.''
Events change the ACL2 logical world (see world). Indeed, the only way
to change the ACL2 world is via the successful evaluation of an event
function. Every time the world is changed by an event, a landmark is
left on the world and it is thus possible to identify the world
``as of'' the evaluation of a given event. An event may introduce new logical
names. Some events introduce no new names (e.g., `verify-guards`), some
introduce exactly one (e.g., `defmacro` and `defthm`), and some
may introduce many (e.g., `encapsulate` ).

ACL2 typically completes processing of an event by printing a summary. Unless proofs are skipped (see ld-skip-proofsp) or summary output is inhibited (see set-inhibit-output-lst), information about the proof attempt (if any) is printed that includes a list of rules used, a summary of warnings, and the number of ``prover steps'' (if any; see with-prover-step-limit). A breakdown of the time used is also printed, which by default is runtime (cpu time), but can be changed to realtime (wall clock time); see get-internal-time.

See embedded-event-form for a discussion of events permitted in books.

- Defun
- Define a function symbol
- Table
- User-managed tables
- Memoize
- Turn on memoization for a specified function
- Make-event
- Evaluate (expand) a given form and then evaluate the result
- Include-book
- Load the events in a file
- Encapsulate
- Hide some events and/or constrain some functions
- Defun-sk
- Define a function whose body has an outermost quantifier
- Defttag
- Introduce a trust tag (ttag)
- Verify-guards
- Verify the guards of a function
- Defpkg
- Define a new symbol package
- Mutual-recursion
- Define some mutually recursive functions
- Defattach
- Execute constrained functions using corresponding attached functions
- Defstobj
- Define a new single-threaded object
- Defchoose
- Define a Skolem (witnessing) function
- Defabsstobj
- Define a new abstract single-threaded object
- Progn
- Evaluate some events
- Redundant-events
- Allowing a name to be introduced ``twice''
- Verify-termination
- Convert a function from :program mode to :logic mode
- Defmacro
- Define a macro
- In-theory
- Designate ``current'' theory (enabling its rules)
- Defconst
- Define a constant
- Embedded-event-form
- Forms that may be embedded in other events
- Value-triple
- Compute a value, optionally checking that it is not
nil - Skip-proofs
- Skip proofs for a given form — a quick way to introduce unsoundness
- Comp
- Compile some ACL2 functions
- Local
- Hiding an event in an encapsulation or book
- Defthm
- Prove and name a theorem
- Progn!
- Evaluate some forms, not necessarily events
- Defevaluator
- Introduce an evaluator function
- Assert-event
- Assert that a given form returns a non-
nil value - Theory-invariant
- User-specified invariants on theories
- Defun-inline
- Define a potentially inlined function symbol and associated macro
- Define-trusted-clause-processor
- Define a trusted (unverified) goal-level simplifier
- Project-dir-alist
- Support for moving project directories (also
:dir arguments) - Partial-encapsulate
- Introduce functions with some constraints unspecified
- Defproxy
- Define a non-executable
: `program`-mode function for attachment - Defexec
- Attach a terminating executable function to a definition
- Defun-nx
- Define a non-executable function symbol
- Defthmg
- Variant of
`defthm`supporting guard verification - Logical-name
- A name created by a logical event
- Defpun
- Define a tail-recursive function symbol
- Defabbrev
- A convenient form of macro definition for simple expansions
- Add-custom-keyword-hint
- Add a new custom keyword hint
- Defrec
- Introduce a record structure, like a
struct in C. - Regenerate-tau-database
- Regenerate the tau database relative to the current enabled theory
- Name
- Syntactic rules on logical names
- Deftheory
- Define a theory (to enable or disable a set of rules)
- Deftheory-static
- Define a `static' theory (to enable or disable a set of rules)
- Defcong
- Prove congruence rule
- Defaxiom
- Add an axiom
- Evisc-table
- Support for abbreviated output
- Defund
- Define a function symbol and then disable it
- Verify-guards+
- Verify the guards of a function
- Profile
- Turn on profiling for one function
- Defequiv
- Prove that a function is an equivalence relation
- Defmacro-untouchable
- Define an ``untouchable'' macro
- Defthmr
- Submit a theorem, as a rewrite rule only if possible.
- Defstub
- Stub-out a function symbol
- Deflabel
- Build a landmark
- Defrefinement
- Prove that
equiv1 refinesequiv2 - In-arithmetic-theory
- Designate theory for some rewriting done for non-linear arithmetic
- Defabsstobj-missing-events
- Obtain the events needed to admit a
`defabsstobj`event - Defthmd
- Prove and name a theorem and then disable it
- Set-body
- Set the definition body
- Unmemoize
- Turn off memoization for the specified function
- Defun-notinline
- Define a not-to-be-inlined function symbol and associated macro
- Dump-events
- Dump events to a file.
- Defund-nx
- Define a disabled non-executable function symbol
- Defun$
- Define a function symbol and generate a warrant
- Remove-custom-keyword-hint
- Remove a custom keyword hint
- Dft
- Provide an explicit proof, for example chaining equalities
- Defthy
- Define a theory (to enable or disable a set of rules)
- Defund-notinline
- Define a disabled, not-to-be-inlined function symbol and associated macro
- Defnd
- disabled definition with guard
t - Defn
- Definition with guard
t - Defund-inline
- Define a potentially disabled, inlined function symbol and associated macro
- Defmacro-last
- Define a macro that returns its last argument, but with side effects
- Defdoc
- Deprecated event (formerly for adding documentation)