Notation | Description | Example |
---|---|---|
Γ | The current typing environment | Γ |
∅ | The empty typing environment | ∅ |
Γ, x | The typing environment Γ extended with the variable x [3] | Γ, x where x ∉ dom(Γ) |
dom(Γ) | The set of distinct variables in Γ | dom((∅, x, y)) = { x, y } |
Γ ⊢ P | The environment Γ implies P | Γ ⊢ 23 : ℕ (in the current typing environment, 23 is of type ℕ) |
Γ ⊢ ◇ | The environment Γ is well-formed | ∅ ⊢ ◇ (the empty typing environment is well-formed) |