The sequents above the line are the premises that must be fulfilled for the rule to be applied, yielding the conclusion: the sequents below the line. This can be read as: if expression has type in environment, for all , then the expression will have an environment and type .
For example, a simple language to perform arithmetic calculations on real numbers may have the following rules
A type rule may have no premises, and usually the line is omitted in these cases. A type rule may also change an environment by adding new variables to a previous environment; for example, a declaration may have the following type rule, where a new variable ,
with type , is added to :
Here the syntax of the let expression is that of Standard ML. Thus type rules can be used to derive the types of composed expressions, much like in natural deduction.