Next: The Syntax Lists
Up: The Theory Environment
Previous: The Theory Environment
The theory environment consists of the constant and operator
declaration list, the master theorem list, and some satellite
declaration lists and lists containing syntactical information. A
theory has a name which associates it with a file.
- A list of operator precedences. Parity of the
precedence determines left/right associativity (even gives right,
odd left). Default precedence of all operators is 0.
- Default left arguments:
- A list of default left arguments for
- There is a list of declarations of constants,
operators, and free variable operators (the last only for relative
typing purposes; free variable operators which do not need to be
typed do not need to be declared).
- Opacity declarations:
- A list of operators declared opaque.
- A list of names of theorems which are intended to
be proved; needed to make recursive tactics possible while
preserving declaration checking for embedded theorems.
- A list of constants and operators with the
theorems which define them; the name of the theorem will be the same
as the name of the defined object, if it is a constant.
- Functional programs:
- A list of automatic bindings of theorems
to constants and operators, implementing functional programming in
the tactic language.
- There is a list of theorems; this also includes
images of current and old saved proof environments. The structure
of an individual theorem parallels the structure of a proof
environment as noted above, with the addition of the list of
theorems supporting the module system. Proof environments saved on
the theorem list lose ``position of selected subterm'' information,
since this is the one item in the structure of a proof environment
that is not found in a theorem.
Fri Sep 5 16:28:58 MDT 1997