| | | B.4.1 I:T=E: Declare Value |
I:T
I:T=E
A value declaration may not only be issued in declaration mode but also in proving mode. It extends the current proof state by a single child state whose environment contains the declaration implementing the rule
[E, I:T=E] A, ... |- B, ...
---------------------------
[E] A, ... |- B, ...
An additional proof state may be generated for a type checking condition corresponding to the value A and the matching of its type to T.
| | | B.4.1 I:T=E: Declare Value |