		Search-engine friendly clone of the ACL2 documentation.

System-utilities-non-built-in

System utilities related to the ACL2 system.

These are useful for system programming, e.g. to build tools that generate new events based on existing events.

These (non-built-in) utilities complement the built-in system utilities.

Subtopics

Pseudo-event-formp: Recognize well-formed event forms.
Pseudo-event-form-listp: Recognize true lists of well-formed event forms.
Directed-untranslate: Create a user-level form that reflects a given user-level form's structure.
Irrelevant-formals-info: Determine whether irrelevant-formals are OK in definitions.
Context-message-pair: A common ACL2 programming idiom: error-triples without state
Numbered-names: Utilities for numbered names.
Prove$: A way to call the prover from a program
Minimize-ruler-extenders: Minimize the ruler-extenders necessary to admit a definition.
Paired-names: Utilities for paired names.
Orelse: Evaluate an event and, if it fails, then evaluate a second event
Fresh-name-in-world-with-$s: Append as many $ signs to a name as needed to make the name new in the world, i.e. not already in use, and not among a given list of names to avoid.
Encapsulate-report-errors: Run encapsulate, but with a helpful error at the first failure of one of its top-level events (if any).
On-failure: Run an event, printing a custom error message if it fails.
Chk-irrelevant-formals-ok: Check irrelevant-formals in definitions.
Named-formulas: Utilities for named formulas.
Pseudo-event-landmarkp: Recognize event landmarks in the ACL2 world.
All-program-fns: All :program-mode functions in a given world.
All-logic-fns: All :logic-mode functions in a given world.
Trans-eval-error-triple: An ACL2 evaluator for forms that return error-triples
Trans-eval-state: An ACL2 evaluator that returns state
Pseudo-tests-and-callsp: Recognize well-formed tests-and-calls records.
User-interface: Utilities for the user interface of event-generating macros (e.g. program transformations).
Pseudo-command-landmarkp: Recognize command landmarks in the ACL2 world.
Pseudo-tests-and-calls-listp: Recognize true lists of well-formed tests-and-calls records.
Pseudo-command-formp: Recognize well-formed command forms.
Orelse*: Evaluate a sequence of events, until one succeeds
Identity-macro: The most trivial macro imaginable