• 水平条表示“[上方]暗示[下方]”。
• 如果 [above] 中有多个表达式，则考虑将它们与一起运算；所有 [以上] 必须是真实的，以保证 [以下]。
• :意味着有类型
• ∈手段在. （同样∉的意思是“不在”。）
• Γ通常用于指代环境或上下文；在这种情况下，它可以被认为是一组类型注释，将标识符与其类型配对。因此x : σ ∈ Γ意味着环境Γ包含x有类型的事实σ。
• ⊢可以读作证明或确定。Γ ⊢ x : σ表示环境Γ确定x有类型σ。
• ,是一种将特定的附加假设包含到环境中的方法Γ。
  因此，Γ, x : τ ⊢ e : τ'意味着 environment Γ，以及具有 type的附加的、压倒一切的假设x``τ，证明了e具有 type τ'。

根据要求：运算符优先级，从高到低：

• 特定于语言的中缀和混缀运算符，例如λ x . e, ∀ α . σ, and τ → τ', let x = e0 in e1, 和用于函数应用的空格。
• :
• ∈ and ∉
• , (left-associative)
• ⊢
• 分隔多个命题的空格（关联）
• 单杠