EVENTS

functions that extend the logic


Parent topic:  Home

ADD-MACRO-ALIAS -- associate a function name with a macro name
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
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
PROGRAM -- to set the default defun-mode to :program
REMOVE-MACRO-ALIAS -- remove the association of a function name with a macro name
SET-COMPILE-FNS -- have each function compiled as you go along.
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-MEASURE-FUNCTION -- set the default measure function symbol
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-MACRO-ALIAS -- associate a function name with a macro name

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`

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

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

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

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

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-MEASURE-FUNCTION -- set the default measure function symbol

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

EVENTS

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

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

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

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

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

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

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-MEASURE-FUNCTION -- set the default measure function symbol

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

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`

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