Definition: Rule
We use the common notation for rules such as type inference rules [1], that is
is the rule’s premises (e.g., the expression to be inferred), the result of the rule. is an optional condition which may be omitted.
Both parts of the rule may contain multiple expressions, which are concatenated via 'and'.
For example, the following
can be read as
if , , and are all true, then is true as well.