EVENTS

functions that extend the logic

Major Section:  ACL2 Documentation

ADD-BINOP -- associate a binary function name with a macro name
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
BINOP-TABLE -- associates binary function with the corresponding macro
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
DEFTHMD -- prove and name a theorem and then disable it
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
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
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-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
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-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-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
WITH-OUTPUT -- suppressing or turning out 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-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

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

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

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

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

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

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

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

WITH-OUTPUT -- suppressing or turning out specified output for an event

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

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

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