- 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. Therefore`x : σ ∈ Γ`

means that the environment`Γ`

includes the fact that`x`

has type`σ`

.`⊢`

can be read as**proves**or determines.`Γ ⊢ x : σ`

means that the environment`Γ`

determines that`x`

has type`σ`

.`,`

is a way of**including**specific additional assumptions into an environment`Γ`

.

Therefore,`Γ, x : τ ⊢ e : τ'`

means that environment`Γ`

,*with the additional, overriding assumption that*, proves that`x`

has type`τ`

`e`

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