| | | A.3.2 Value Declarations |
I: T
I: T = E
This declaration introduces a value constant denoted by the identifier I; the type of the constant is T. The command form I: T does not define the value of I. The command form I: T = E defines the value of I by the value E whose type must match T.
As well determining the type of E as matching the type of E to T may give rise to a type checking condition.
A value declaration may also appear in proving mode.
The declaration may also introduce function or predicate constants which are just value constants with function type. Matching the value type U1 -> U2 to the declaration type T1 -> T2 only succeeds if both T1 equals U1 and T2 equals U2. This is stricter than theoretically necessary (it would suffice to check that T1 is a subtype of U1 and U2 is a subtype of T2) because the decision procedure applied by the system may not accept a looser type discipline.
| | | A.3.2 Value Declarations |