- The horizontal bar means that “[above] implies [below]”.
- If there are multiple expressions in [above], then consider them anded together; all of the [above] must be true in order to guarantee the [below].
:
means has type∈
means is in. (Likewise∉
means “is not in”.)Γ
is usually used to refer to an environment or context; in this case it can be thought of as a set of type annotations, pairing an identifier with its type. Thereforex : σ ∈ Γ
means that the environmentΓ
includes the fact thatx
has typeσ
.⊢
can be read as proves or determines.Γ ⊢ x : σ
means that the environmentΓ
determines thatx
has typeσ
.,
is a way of including specific additional assumptions into an environmentΓ
.
Therefore,Γ, x : τ ⊢ e : τ'
means that environmentΓ
, with the additional, overriding assumption thatx
has typeτ
, proves thate
has typeτ'
.
As requested: operator precedence, from highest to lowest:
- Language-specific infix and mixfix operators, such as
λ x . e
,∀ α . σ
, andτ → τ'
,let x = e0 in e1
, and whitespace for function application. :
∈
and∉
,
(left-associative)⊢
- whitespace separating multiple propositions (associative)
- the horizontal bar