is an expression that has exactly the value of but its type is specified by the type expression (3.3.1.1).
is restricted to expressions whose type does not depend on an argument of that expression. These are the constant relations , , and the empty set .
Another location where the operator can be used is the declaration of bound variables in quantifiers and patterns in lambda expressions. Each identifier can be followed by and the identifier’s type.
Definition
Types
with
WD
Example
The predicate is not correctly typed in Event-B because the types of are not inferable. A valid alternative would be:
The predicate is not correctly typed because the types of and cannot be inferred: A valid alternative (for integers) is:
The following lambda expression uses the operator:
An arguably more readable version without the use of is: