EVENTS

Major Section:  ACL2 Documentation

Some Related Topics

• ADD-CUSTOM-KEYWORD-HINT -- add a new custom keyword hint

• ASSERT-EVENT -- assert that a given form returns a non-nil value

• COMP -- compile some ACL2 functions

• DEFABBREV -- a convenient form of macro definition for simple expansions

• DEFABSSTOBJ -- define a new abstract single-threaded object

• DEFABSSTOBJ-MISSING-EVENTS -- obtain the events needed to admit a defabsstobj event

• DEFATTACH -- execute constrained functions using corresponding attached functions

• DEFAXIOM -- add an axiom

• DEFCHOOSE -- define a Skolem (witnessing) function

• DEFCONG -- prove congruence rule

• DEFCONST -- define a constant

• DEFDOC -- add a documentation topic

• DEFEQUIV -- prove that a function is an equivalence relation

• DEFEVALUATOR -- introduce an evaluator function

• DEFEXEC -- attach a terminating executable function to a definition

• DEFINE-TRUSTED-CLAUSE-PROCESSOR -- define a trusted (unverified) goal-level simplifier

• DEFLABEL -- build a landmark and/or add a documentation topic

• DEFMACRO -- define a macro

• DEFMACRO-LAST -- define a macro that returns its last argument, but with side effects

• DEFN -- definition with guard t

• DEFND -- disabled definition with guard t

• DEFPKG -- define a new symbol package

• DEFPROXY -- define a non-executable :program-mode function for attachment

• DEFPUN -- define a tail-recursive function symbol

• DEFREFINEMENT -- prove that equiv1 refines equiv2

• DEFSTOBJ -- define a new single-threaded object

• DEFSTUB -- stub-out a function symbol

• 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)

• DEFTHM -- prove and name a theorem

• DEFTHMD -- prove and name a theorem and then disable it

• DEFTTAG -- introduce a trust tag (ttag)

• DEFUN -- define a function symbol

• DEFUN-INLINE -- define a potentially inlined function symbol and associated macro

• DEFUN-NOTINLINE -- define a not-to-be-inlined function symbol and associated macro

• DEFUN-NX -- define a non-executable function symbol

• DEFUN-SK -- define a function whose body has an outermost quantifier

• DEFUND -- define a function symbol and then disable it

• DEFUND-INLINE -- define a potentially disabled, inlined function symbol and associated macro

• DEFUND-NOTINLINE -- define a disabled, not-to-be-inlined function symbol and associated macro

• ENCAPSULATE -- hide some events and/or constrain some functions

• EVISC-TABLE -- support for abbreviated output

• IN-ARITHMETIC-THEORY -- designate theory for some rewriting done for non-linear arithmetic

• IN-THEORY -- designate ``current'' theory (enabling its rules)

• INCLUDE-BOOK -- load the events in a file

• LOCAL -- hiding an event in an encapsulation or book

• MAKE-EVENT -- evaluate (expand) a given form and then evaluate the result

• MEMOIZE -- turn on memoization for a specified function

• MUTUAL-RECURSION -- define some mutually recursive functions

• PROFILE -- turn on profiling for one function

• PROGN -- evaluate some events

• PROGN! -- evaluate some forms, not necessarily events

• REGENERATE-TAU-DATABASE -- regenerate the tau database relative to the current enabled theory

• REMOVE-CUSTOM-KEYWORD-HINT -- remove a custom keyword hint

• RESTORE-MEMOIZATION-SETTINGS -- restore the saved memoization settings

• SAVE-AND-CLEAR-MEMOIZATION-SETTINGS -- save and remove the current memoization settings

• SET-BODY -- set the definition body

• TABLE -- user-managed tables

• THEORY-INVARIANT -- user-specified invariants on theories

• UNMEMOIZE -- turn off memoization for the specified function

• VALUE-TRIPLE -- compute a value, optionally checking that it is not nil

• VERIFY-GUARDS -- verify the guards of a function

• VERIFY-GUARDS+ -- verify the guards of a function

• VERIFY-TERMINATION -- convert a function from :program mode to :logic mode

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.