Events
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.
Subtopics
- 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)
- Defstobj
- Define a new single-threaded object
- Defpkg
- Define a new symbol package
- Defattach
- Execute constrained functions using corresponding attached functions
- Defchoose
- Define a Skolem (witnessing) function
- Defabsstobj
- Define a new abstract single-threaded object
- Progn
- Evaluate some events
- Verify-termination
- Convert a function from :program mode to :logic mode
- Redundant-events
- Allowing a name to be introduced ``twice''
- Defconst
- Define a constant
- 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
- Name
- Syntactic rules on logical names
- Defrec
- Introduce a record structure, like a struct in C.
- Add-custom-keyword-hint
- Add a new custom keyword hint
- Regenerate-tau-database
- Regenerate the tau database relative to the current enabled theory
- Defcong
- Prove congruence rule
- 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)
- 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.
- Add-global-stobj
- Add a global stobj with a given name
- Defstub
- Stub-out a function symbol
- Defrefinement
- Prove that equiv1 refines equiv2
- Deflabel
- Build a landmark
- In-arithmetic-theory
- Designate theory for some rewriting done for non-linear arithmetic
- Unmemoize
- Turn off memoization for the specified function
- 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
- 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)
- Remove-global-stobj
- Remove a global stobj with a given name
- 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
