和类型表示两种类型之间的选择：和类型的一个元素是这两种类型之一的元素，并配有指示其来源类型的标记。 和类型也称为不相交并集、可辨识联合或标记联合。 和类型的构造子也称为单射；在数学上，它们可以被视为从每个被加数到和类型的单射函数。
和类型有两种变体：
手动编写的 Lean 代码几乎总是只使用 Sum，而 PSum 则作为证明自动化实现的一部分使用。
这是因为它施加了宇宙层级合一无法解决的棘手约束。
特别地，该类型位于宇宙 Sort (max 1 u v) 中，这可能会给宇宙层级合一带来问题，因为等式 max 1 u v = ?u + 1 在层级算术中无解。
PSum 通常仅用于构造任意类型之和的自动化中。
类型 α 和 β 的不交并，通常写作 α ⊕ β。
α ⊕ β 的元素要么是由 a : α 经 Sum.inl 包装得到的值，要么是由 b : β 经 Sum.inr 包装得到的值。α ⊕ β 不等价于 α 与 β 的集合论并集，因为其值还包含从两种类型中选择了哪一种的信息。单元素集合与自身的并集只有一个元素，而 Unit ⊕ Unit 包含不同的值 inl () 和 inr ()。
构造子
Sum.inl.{u, v} {α : Type u} {β : Type v} (val : α) : α ⊕ β
到和类型 α ⊕ β 的左注入。
Sum.inr.{u, v} {α : Type u} {β : Type v} (val : β) : α ⊕ β
到和类型 α ⊕ β 的右注入。
任意排序 α β 或 α ⊕' β 的不相交并集。
它与 α ⊕ β 的不同之处在于，它允许 α 和 β 具有任意排序 Sort u 和 Sort v，而不是将它们限制为 Type u 和 Type v。这意味着它可以用在一侧是命题的情况下，例如 True ⊕' Nat。然而，由此产生的宇宙级约束通常比 Sum 产生的约束更难解决。
构造子
PSum.inl.{u, v} {α : Sort u} {β : Sort v} (val : α) : α ⊕' β
到和类型 α ⊕' β 的左注入。
PSum.inr.{u, v} {α : Sort u} {β : Sort v} (val : β) : α ⊕' β
到和类型 α ⊕' β 的右注入。
和类型主要与模式匹配一起使用，而不是来自 API 的显式函数调用。
因此，它们的主要 API 是构造子 inl 和 inr。
检查总和是否为左注入inl。
检查总和是否是正确的注入 inr。
Sum.elim.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) : α ⊕ β → γSum.elim.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) : α ⊕ β → γ
在检查存在哪个构造函数后，对应用适当函数 f 或 g 的求和进行案例分析。
从已知为 inl 的总和中检索内容。
检查总和是否为左注入 inl，如果是，则检索其内容。
从已知为 inr 的总和中检索内容。
检查总和是否是正确的注入 inr，如果是，则检索其内容。
Sum.map.{u_1, u_2, u_3, u_4} {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β'Sum.map.{u_1, u_2, u_3, u_4} {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β'
根据每种类型的函数转换总和。
该函数将 α ⊕ β 映射到 α' ⊕ β'，将 α 发送到 α'，将 β 发送到 β'。
Inhabited 对 Sum 和 PSum 的定义没有被注册为实例。
这是因为有两种不同的方法来构造默认值（通过 inl 或 inr），而实例合成可能会导致任一选择。
结果可能是两种写法完全相同的项却精译出不同的结果，并且它们不是定义等价的。
这两种类型都有 Nonempty 实例，由于证明无关性，选择 inl 还是 inr 并不重要。
这足以启用 partial 函数。
对于需要 Inhabited 实例的情况，例如使用 panic! 的程序，可以通过 Lean.Parser.Term.have : termhave 或 Lean.Parser.Term.let : termlet 将其添加到局部上下文中来显式使用该实例。
在 Lean 的逻辑中，Lean.Parser.Term.panic : termpanic! 等同于在其类型的 Inhabited 实例中指定的默认值。
这意味着该类型必须具有这样的实例——Nonempty 实例结合选择公理会使程序变得不可计算。
积类型具有合适的实例：
example : Nat × String := panic! "Can't find it"
和类型默认情况下没有：
example : Nat ⊕ String := panic! "Can't find it"
可以使用 Lean.Parser.Term.have : termhave 使所需的实例对实例合成可用：
example : Nat ⊕ String :=
have : Inhabited (Nat ⊕ String) := Sum.inhabitedLeft
panic! "Can't find it"
如果总和中的左侧类型被占据，则总和被占据。
当左类型和右类型都存在时，这不是避免非规范实例的实例。
如果总和中存在正确的类型，那么总和就存在。
当左类型和右类型都存在时，这不是避免非规范实例的实例。
如果总和中的左侧类型被占据，则总和被占据。
当左类型和右类型都存在时，这不是避免非规范实例的实例。