EVENTS

functions that extend the logic

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
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
DEFPKG -- define a new symbol package
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)
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-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
ENCAPSULATE -- constrain some functions and/or hide some events
EVISC-TABLE -- support for abbreviated output
IN-ARITHMETIC-THEORY -- designate ``current'' theory for some rewriting done in 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 one function
MUTUAL-RECURSION -- define some mutually recursive functions
PROGN -- evaluate some events
PROGN! -- evaluate some forms, not necessarily events
REDO-FLAT -- redo up through a failure in an encapsulate or progn
REMOVE-CUSTOM-KEYWORD-HINT -- remove a custom keyword hint
SET-BODY -- set the definition body
SHOW-CUSTOM-KEYWORD-HINT-EXPANSION -- print out custom keyword hints when they are expanded
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-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 data base (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 that includes a breakdown of time used and, 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) including a list of rules used and a summary of warnings. A detail: The time is calculated using Common Lisp function get-internal-run-time, which may ignore calls to external tools (see sys-call and see clause-processor).

EVENTS

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

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

DEFPKG -- define a new symbol package

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)

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

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

EVISC-TABLE -- support for abbreviated output

IN-ARITHMETIC-THEORY -- designate ``current'' theory for some rewriting done in 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 one function

MUTUAL-RECURSION -- define some mutually recursive functions

PROGN -- evaluate some events

PROGN! -- evaluate some forms, not necessarily events

REDO-FLAT -- redo up through a failure in an encapsulate or progn

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

SET-BODY -- set the definition body

SHOW-CUSTOM-KEYWORD-HINT-EXPANSION -- print out custom keyword hints when they are expanded

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-TERMINATION -- convert a function from :program mode to :logic mode

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

DEFREFINEMENT -- prove that `equiv1` refines `equiv2`

REDO-FLAT -- redo up through a failure in an `encapsulate` or `progn`

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