EVENTS

functions that extend the logic

Major Section:  ACL2 Documentation

ADD-BINOP -- associate a binary function name with a macro name
ADD-MACRO-ALIAS -- associate a function name with a macro name
ADD-NTH-ALIAS -- associate one symbol with another for printing of nth/update-nth terms
DEFABBREV -- a convenient form of macro definition for simple expansions
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
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
DEFUN -- define a function symbol
DEFUN-SK -- define a function whose body has an outermost quantifier
ENCAPSULATE -- constrain some functions and/or hide some events
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
LOGIC -- to set the default defun-mode to :logic
MACRO-ALIASES-TABLE -- a table used to associate function names with macro names
MUTUAL-RECURSION -- define some mutually recursive functions
NTH-ALIASES-TABLE -- a table used to associate names for nth/update-nth printing
PROGRAM -- to set the default defun-mode to :program
PUSH-UNTOUCHABLE -- add name or list of names to the list of untouchable symbols
REMOVE-BINOP -- remove the association of a binary function name with a macro name
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
SET-BACKCHAIN-LIMIT -- Sets the backchain-limit used by the rewriter
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-IGNORE-OK -- allow unused formals and locals without an ignore declaration
SET-INHIBIT-WARNINGS -- control warnings
SET-INVISIBLE-FNS-ALIST -- set the invisible functions alist
SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions
SET-LET*-ABSTRACTIONP -- to shorten many prettyprinted clauses
SET-MEASURE-FUNCTION -- set the default measure function symbol
SET-NU-REWRITER-MODE -- to turn on and off the nu-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
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 ).

EVENTS

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

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

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

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

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

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

DEFUN -- define a function symbol

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

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

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

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

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

MUTUAL-RECURSION -- define some mutually recursive functions

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

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

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

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

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

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

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-IGNORE-OK -- allow unused formals and locals without an ignore declaration

SET-INHIBIT-WARNINGS -- control warnings

SET-INVISIBLE-FNS-ALIST -- set the invisible functions alist

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

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

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

SET-NU-REWRITER-MODE -- to turn on and off the nu-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

VERIFY-GUARDS -- verify the guards of a function

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

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

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

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

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

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

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

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