| | | B.4.4 expand: Expand Definitions |
expand I1, I2, ...
expand I1, I2, ... in
F1, F2, ...
In proving mode.
The command takes a list of identifiers I1, I2, ... denoting names of constants (functions, predicates) whose values have been explicitly defined in their declarations. It generates a single child state by expanding all occurrences of these constants in the current proof state to their values. If the expansion yields new occurrences of value constants whose names occur among these identifiers, these occurrences are also expanded, such that the resulting state is free of value constants with these names. The command may be also provided with a list of labels F1, F2, ... of formulas of the current proof state; in this case, only the occurrences of the constants in these formulas are expanded. If some identifier does not denote the name of a value constant with an explicit definition or some label does not denote a formula in the current state, no child state is generated.
| | | B.4.4 expand: Expand Definitions |