EVENTS

functions that extend the logic

Major Section:  ACL2 Documentation

ADD-BINOP -- associate a binary function name with a macro name
ADD-DEFAULT-HINTS -- add to the default hints
ADD-DEFAULT-HINTS! -- add to the default hints non-locally
ADD-DIVE-INTO-MACRO -- associate proof-checker diving function with macro name
ADD-INCLUDE-BOOK-DIR -- associate directory to keyword for include-book's :dir argument
ADD-INVISIBLE-FNS -- make some unary functions invisible to the loop-stopper algorithm
ADD-MACRO-ALIAS -- associate a function name with a macro name
ADD-MATCH-FREE-OVERRIDE -- set :match-free value to :once or :all in existing rules
ADD-NTH-ALIAS -- associate one symbol with another for printing of nth/update-nth terms
ASSERT-EVENT -- assert that a given form returns a non-nil value
BINOP-TABLE -- associates binary function with the corresponding macro
COMP -- compile some ACL2 functions
DEFABBREV -- a convenient form of macro definition for simple expansions
DEFAULT-HINTS-TABLE -- a table used to provide hints for proofs
DEFAXIOM -- add an axiom
DEFCHOOSE -- define a Skolem (witnessing) function
DEFCONG -- prove that one equivalence relation preserves another in a given
argument position of a given function
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
DEFLABEL -- build a landmark and/or add a documentation topic
DEFMACRO -- define a macro
DEFPKG -- define a new symbol package
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-SK -- define a function whose body has an outermost quantifier
DEFUND -- define a function symbol and then disable it
DELETE-INCLUDE-BOOK-DIR -- remove association of keyword for include-book's :dir argument
DIVE-INTO-MACROS-TABLE -- right-associated function information for the proof-checker
ENCAPSULATE -- constrain some functions and/or hide some events
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
INVISIBLE-FNS-TABLE -- functions that are invisible to the loop-stopper algorithm
LOCAL -- hiding an event in an encapsulation or book
LOGIC -- to set the default defun-mode to :logic
MACRO-ALIASES-TABLE -- a table used to associate function names with macro names
MAKE-EVENT -- evaluate (expand) a given form and then evaluate the result
MUTUAL-RECURSION -- define some mutually recursive functions
NTH-ALIASES-TABLE -- a table used to associate names for nth/update-nth printing
PROGN -- evaluate some events
PROGN! -- evaluate some forms, not necessarily events
PROGRAM -- to set the default defun-mode to :program
PUSH-UNTOUCHABLE -- add name or list of names to the list of untouchable symbols
REDO-FLAT -- redo up through a failure in an encapsulate or progn
REMOVE-BINOP -- remove the association of a binary function name with a macro name
REMOVE-DEFAULT-HINTS -- remove from the default hints
REMOVE-DEFAULT-HINTS! -- remove from the default hints non-locally
REMOVE-DIVE-INTO-MACRO -- removes association of proof-checker diving function with macro name
REMOVE-INVISIBLE-FNS -- make some unary functions no longer invisible
REMOVE-MACRO-ALIAS -- remove the association of a function name with a macro name
REMOVE-NTH-ALIAS -- remove the association of one symbol with another for printing of nth/update-nth terms
REMOVE-UNTOUCHABLE -- remove name or list of names to the list of untouchable symbols
RESET-PREHISTORY -- reset the prehistory
SET-BACKCHAIN-LIMIT -- Sets the backchain-limit used by the rewriter
SET-BODY -- set the definition body
SET-BOGUS-MUTUAL-RECURSION-OK -- allow unnecessary ``mutual recursion''
SET-CASE-SPLIT-LIMITATIONS -- set the case-split-limitations
SET-COMPILE-FNS -- have each function compiled as you go along.
SET-DEFAULT-BACKCHAIN-LIMIT -- sets the default backchain-limit used when admitting a rule
SET-DEFAULT-HINTS -- set the default hints
SET-DEFAULT-HINTS! -- set the default hints non-locally
SET-ENFORCE-REDUNDANCY -- require most events to be redundant
SET-IGNORE-OK -- allow unused formals and locals without an ignore or ignorable declaration
SET-INHIBIT-WARNINGS -- control warnings
SET-INVISIBLE-FNS-TABLE -- set the invisible functions table
SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions
SET-LET*-ABSTRACTIONP -- to shorten many prettyprinted clauses
SET-MATCH-FREE-DEFAULT -- provide default for :match-free in future rules
SET-MATCH-FREE-ERROR -- control error vs. warning when :match-free is missing
SET-MEASURE-FUNCTION -- set the default measure function symbol
SET-NON-LINEARP -- to turn on or off non-linear arithmetic reasoning
SET-NU-REWRITER-MODE -- to turn on and off the nu-rewriter
SET-REWRITE-STACK-LIMIT -- Sets the rewrite stack depth used by the rewriter
SET-STATE-OK -- allow the use of STATE as a formal parameter
SET-VERIFY-GUARDS-EAGERNESS -- the eagerness with which guard verification is tried.
SET-WELL-FOUNDED-RELATION -- set the default well-founded relation
TABLE -- user-managed tables
TERM-TABLE -- a table used to validate meta rules
THEORY-INVARIANT -- user-specified invariants on theories
USER-DEFINED-FUNCTIONS-TABLE -- an advanced table used to replace certain system functions
VERIFY-GUARDS -- verify the guards of a function
VERIFY-TERMINATION -- convert a function from :program mode to :logic mode
WITH-OUTPUT -- suppressing or turning on specified output for an event

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

EVENTS

ADD-BINOP -- associate a binary function name with a macro name

ADD-DEFAULT-HINTS -- add to the default hints

ADD-DEFAULT-HINTS! -- add to the default hints non-locally

ADD-DIVE-INTO-MACRO -- associate proof-checker diving function with macro name

ADD-INCLUDE-BOOK-DIR -- associate directory to keyword for include-book's :dir argument

ADD-INVISIBLE-FNS -- make some unary functions invisible to the loop-stopper algorithm

ADD-MACRO-ALIAS -- associate a function name with a macro name

ADD-MATCH-FREE-OVERRIDE -- set :match-free value to :once or :all in existing rules

ADD-NTH-ALIAS -- associate one symbol with another for printing of nth/update-nth terms

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

BINOP-TABLE -- associates binary function with the corresponding macro

COMP -- compile some ACL2 functions

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

DEFAULT-HINTS-TABLE -- a table used to provide hints for proofs

DEFAXIOM -- add an axiom

DEFCHOOSE -- define a Skolem (witnessing) function

DEFCONG -- prove that one equivalence relation preserves another in a given argument position of a given function

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

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

DEFMACRO -- define a macro

DEFPKG -- define a new symbol package

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-SK -- define a function whose body has an outermost quantifier

DEFUND -- define a function symbol and then disable it

DELETE-INCLUDE-BOOK-DIR -- remove association of keyword for include-book's :dir argument

DIVE-INTO-MACROS-TABLE -- right-associated function information for the proof-checker

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

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

INVISIBLE-FNS-TABLE -- functions that are invisible to the loop-stopper algorithm

LOCAL -- hiding an event in an encapsulation or book

LOGIC -- to set the default defun-mode to :logic

MACRO-ALIASES-TABLE -- a table used to associate function names with macro names

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

MUTUAL-RECURSION -- define some mutually recursive functions

NTH-ALIASES-TABLE -- a table used to associate names for nth/update-nth printing

PROGN -- evaluate some events

PROGN! -- evaluate some forms, not necessarily events

PROGRAM -- to set the default defun-mode to :program

PUSH-UNTOUCHABLE -- add name or list of names to the list of untouchable symbols

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

REMOVE-BINOP -- remove the association of a binary function name with a macro name

REMOVE-DEFAULT-HINTS -- remove from the default hints

REMOVE-DEFAULT-HINTS! -- remove from the default hints non-locally

REMOVE-DIVE-INTO-MACRO -- removes association of proof-checker diving function with macro name

REMOVE-INVISIBLE-FNS -- make some unary functions no longer invisible

REMOVE-MACRO-ALIAS -- remove the association of a function name with a macro name

REMOVE-NTH-ALIAS -- remove the association of one symbol with another for printing of nth/update-nth terms

REMOVE-UNTOUCHABLE -- remove name or list of names to the list of untouchable symbols

RESET-PREHISTORY -- reset the prehistory

SET-BACKCHAIN-LIMIT -- Sets the backchain-limit used by the rewriter

SET-BODY -- set the definition body

SET-BOGUS-MUTUAL-RECURSION-OK -- allow unnecessary ``mutual recursion''

SET-CASE-SPLIT-LIMITATIONS -- set the case-split-limitations

SET-COMPILE-FNS -- have each function compiled as you go along.

SET-DEFAULT-BACKCHAIN-LIMIT -- sets the default backchain-limit used when admitting a rule

SET-DEFAULT-HINTS -- set the default hints

SET-DEFAULT-HINTS! -- set the default hints non-locally

SET-ENFORCE-REDUNDANCY -- require most events to be redundant

SET-IGNORE-OK -- allow unused formals and locals without an ignore or ignorable declaration

SET-INHIBIT-WARNINGS -- control warnings

SET-INVISIBLE-FNS-TABLE -- set the invisible functions table

SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions

SET-LET*-ABSTRACTIONP -- to shorten many prettyprinted clauses

SET-MATCH-FREE-DEFAULT -- provide default for :match-free in future rules

SET-MATCH-FREE-ERROR -- control error vs. warning when :match-free is missing

SET-MEASURE-FUNCTION -- set the default measure function symbol

ADD-DEFAULT-HINTS! -- add to the default hints non-`local`ly

ADD-INCLUDE-BOOK-DIR -- associate directory to keyword for `include-book`'s `:dir` argument

ADD-MATCH-FREE-OVERRIDE -- set `:match-free` value to `:once` or `:all` in existing rules

ADD-NTH-ALIAS -- associate one symbol with another for printing of `nth`/`update-nth` terms

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

DEFCONG -- prove that one equivalence relation preserves another in a given
argument position of a given function

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

DELETE-INCLUDE-BOOK-DIR -- remove association of keyword for `include-book`'s `:dir` argument

LOGIC -- to set the default defun-mode to `:logic`

PROGRAM -- to set the default defun-mode to `:program`

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

REMOVE-DEFAULT-HINTS! -- remove from the default hints non-`local`ly

REMOVE-NTH-ALIAS -- remove the association of one symbol with another for printing of `nth`/`update-nth` terms

SET-DEFAULT-HINTS! -- set the default hints non-`local`ly

SET-IGNORE-OK -- allow unused formals and locals without an `ignore` or `ignorable` declaration

SET-MATCH-FREE-DEFAULT -- provide default for `:match-free` in future rules

SET-MATCH-FREE-ERROR -- control error vs. warning when `:match-free` is missing