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
- Verify-guards
- Verify the guards of a function
- Table
- User-managed tables
- Mutual-recursion
- Define some mutually recursive functions
- 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)
- Defpkg
- Define a new symbol package
- Defattach
- Execute constrained functions using corresponding attached functions
- Defstobj
- Define a new single-threaded object
- Defchoose
- Define a Skolem (witnessing) function
- Progn
- Evaluate some events
- Defabsstobj
- Define a new abstract single-threaded object
- Verify-termination
- Convert a function from :program mode to :logic mode
- Defconst
- Define a constant
- Redundant-events
- Allowing a name to be introduced ``twice''
- Defmacro
- Define a macro
- Skip-proofs
- Skip proofs for a given form — a quick way to introduce unsoundness
- In-theory
- Designate ``current'' theory (enabling its rules)
- Embedded-event-form
- Forms that may be embedded in other events
- Value-triple
- Compute a value, optionally checking that it is not
nil - 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
- Theory-invariant
- User-specified invariants on theories
- Assert-event
- Assert that a given form returns a non-
nil value - Defun-inline
- Define a potentially inlined function symbol and associated macro
- Project-dir-alist
- Support for moving project directories (also
:dir arguments) - Partial-encapsulate
- Introduce functions with some constraints unspecified
- Define-trusted-clause-processor
- Define a trusted (unverified) goal-level simplifier
- 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 - Defpun
- Define a tail-recursive function symbol
- Defabbrev
- A convenient form of macro definition for simple expansions
- Set-table-guard
- Set the
:guard for a table - Defrec
- Introduce a record structure, like a
struct in C. - Name
- Syntactic rules on logical names
- Add-custom-keyword-hint
- Add a new custom keyword hint
- Regenerate-tau-database
- Regenerate the tau database relative to the current enabled theory
- 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
- Defund
- Define a function symbol and then disable it
- Evisc-table
- Support for abbreviated output
- Verify-guards+
- Verify the guards of a function
- Logical-name
- A name created by a logical event
- 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
- Fake-event
- Execute an event form without affecting the world.
- 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
- Functions-after
- Function symbols introduced after a given event name
- Macros-after
- Macro names introduced after a given event name
- 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