Next: Predeclared theorems:
Up: Predeclared objects:
Previous: Predeclared objects:
- true false:
- Truth values.
- P1 P2 Id:
- The projection operators and the identity
function; also their defining theorems. There are variants p1
and p2 of P1 and P2 which are used by the
higher-order matching mechanism; the lower-case variants are automatically
applied by the tactic interpreter where possible (as if they were
functionally programmed with their defining theorems).
- Equality (also a built in tactic).
- Function application (also application of
parameterized tactics to their arguments).
- Application of unstratified ``class functions''; used
for refinements of higher order matching and extension of first-order
- : Function composition.
- Ordered pair. List constructor. Also the second component
of the mixfix case expression constructor.
- The first component of the mixfix case expression
constructor. Not really an operator.