Theory-functions
Functions for obtaining or producing theories
Example Calls of Theory Functions:
(universal-theory :here)
(union-theories th1 th2)
(set-difference-theories th1 th2)
The theory functions are documented individually:
The functions (actually, macros) mentioned above are convenient ways to
produce theories. (See theories.) Some, like universal-theory, take a logical name (see logical-name) as an
argument and return the relevant theory as of the time that name was
introduced. Others, like union-theories, take two theories and
produce a new one. See redundant-events for a caution about the use of
logical names in theory expressions.
Theory expressions are generally composed of applications of theory
functions. Formally, theory expressions are expressions that involve, at
most, the free variable world and that when evaluated with world bound to the current ACL2 world (see world) return theories. The ``theory functions'' are actually macros that expand into
forms that involve the free variable world. Thus, for example
(universal-theory :here) actually expands to (universal-theory-fn
:here world) and when that form is evaluated with world bound to the
current ACL2 world, universal-theory-fn scans the ACL2 property
lists and computes the current universal theory. Because the theory functions
all implicitly use world, the variable does not generally appear in
anything the user types.
Subtopics
- Disable
- Deletes names from current theory
- Enable
- Adds names to current theory
- Current-theory
- Currently enabled rules as of logical name
- Syntactically-clean-lambda-objects-theory
- how to specify syntactic cleaning of lambda objects
- Hands-off-lambda-objects-theory
- how to specify no modification of lambda objects
- Rewrite-lambda-objects-theory
- how to specify rewriting of lambda objects
- Theory
- Retrieve named theory
- Universal-theory
- All rules as of logical name
- E/d
- Enable/disable rules
- Executable-counterpart-theory
- Executable-counterpart rules as of logical name
- Function-theory
- Function symbol rules as of logical name
- Set-difference-theories
- Difference of two theories
- Minimal-theory
- A minimal theory to enable
- Ground-zero
- enabled rules in the startup theory
- Union-theories
- Union two theories
- Intersection-theories
- Intersect two theories
