结构体 Subtype 表示某个类型中满足某个谓词的元素。
它在数学与编程中都被广泛使用；在数学中，它的用法类似于子集；在编程中，它允许将关于某个值的已知信息表示为 Lean 逻辑可见的形式。
从语法上看，Subtype 的一个元素类似于由底层类型中的值及其满足该命题的证明所组成的元组。
它与依值有序对类型（Sigma）的区别在于第二个元素是命题的证明而非数据；它与存在量化的区别在于整个 Subtype 是一个类型而不是命题。
尽管它在语法上是一个有序对，Subtype 实际上更应被看作“带有关联证明义务的底层类型元素”。
子类型是 平凡包装器。 因此，在编译后的代码中，它们与底层类型具有完全相同的表示。
满足某个谓词的一个类型中的所有元素。
Subtype p 通常写作 { x : α // p x } 或 { x // p x }，它包含所有 x : α 且 p x 为真的元素。其构造子由值及证明该值满足谓词的证据组成。在运行时代码中，{ x : α // p x } 与 α 具有相同的表示。
存在从 { x : α // p x } 到 α 的强制转换，因此子类型的元素可用于需要底层类型之处。
示例：
{ n : Nat // n % 2 = 0 } 是偶数的类型。
给定 xs : List α，List { x : α // x ∈ xs } 是其所有元素都包含在 xs 中的列表类型。
标识符中记法的约定：
标识符中 { x // p x } 的推荐拼写是 subtype。
构造子
Subtype.mk.{u}
由于 证明无关性 和 η-等价，当底层类型中的元素定义等价时，子类型中的两个元素也定义等价。
在证明中，可以使用 ext 策略将“两个子类型元素相等”的目标化为“它们的值相等”的目标。
尽管内嵌的证明项不同，非空字符串 s1 和 s2 仍然定义等价。
因此，要证明它们相等，不需要做任何分类讨论。
def NonEmptyString := { x : String // x ≠ "" }
def s1 : NonEmptyString :=
⟨"equal", ne_of_beq_false rfl⟩
def s2 : NonEmptyString where
val := "equal"
property :=
fun h =>
List.cons_ne_nil _ _ (String.ext_iff.mp h)
theorem s1_eq_s2 : s1 = s2 := ⊢ s1 = s2 All goals completed! 🐙
非空字符串 s1 与 s2 本身就是定义等价的。
即便不利用这一事实，也可以通过它们内部字符串的相等来证明二者相等。
ext 策略会把“非空字符串相等”的目标转化为“底层字符串相等”的目标。
abbrev NonEmptyString := { x : String // x ≠ "" }
def s1 : NonEmptyString :=
⟨"equal", ne_of_beq_false rfl⟩
def s2 : NonEmptyString where
val := "equal"
property :=
fun h =>
List.cons_ne_nil _ _ (String.ext_iff.mp h)
theorem s1_eq_s2 : s1 = s2 := ⊢ s1 = s2
i✝:Nata✝:Char⊢ s1.val.toList[i✝]? = some a✝ ↔ s2.val.toList[i✝]? = some a✝
i✝:Nata✝:Char⊢ "equal".toList[i✝]? = some a✝ ↔ "equal".toList[i✝]? = some a✝
All goals completed! 🐙
存在从子类型到底层类型的强制转换。 这使得子类型可以用在期望底层类型的地方，本质上等于擦除了“该值满足谓词”的证明。