functions that extend the logic
Major Section:  ACL2 Documentation

Some Related Topics

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 database (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. 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) is printed that includes a list of rules used, a summary of warnings, and the number of ``prover steps'' (if any; see with-prover-step-limit). A breakdown of the time used is also printed, which by default is runtime (cpu time), but can be changed to realtime (wall clock time); see get-internal-time.

See embedded-event-form for a discussion of events permitted in books.