| | | B.1.3 tcc: Print Type Checking Condition |
tcc
In declaration mode.
For type checking a constant declaration, it may be necessary to check a condition which cannot be derived by static type checking but requires actual proving. When in proving mode, such a type checking condition gives rise to an additional proof state with the type checking condition as the goal. When in declaration mode, the system attempts to resolve a type checking condition silently by the application of an automated decision procedure; only if a condition cannot be automatically proved (which may or may not indicate an error), it is displayed to the user. By application of the command tcc, the last generated type checking condition (even if successfully proved) is displayed.
It is questionable whether the information provided by this command is really of interest to the general user. The command was mainly introduced for debugging purposes and will perhaps go away in a future version of the system.
| | | B.1.3 tcc: Print Type Checking Condition |