CoeSort α β 是到 Sort 的强制转换。β 必须是一个宇宙。当 a : α 出现在预期类型的位置，
例如 (x : a) 或 a → a 中时，就会触发该转换。
CoeSort 实例也适用于 CoeOut。
实例构造子
CoeSort.mk.{u, v}
方法
coe : α → β
将类型为 α 的值强制转换到 β；β 必须是一个宇宙。
11.3. 强制转换为 Sort
Lean 精译器会在某些位置期待类型，却未必能预先确定该类型的宇宙。
例如，定义头中冒号后的项可能是命题，也可能是类型。
普通的强制转换机制并不适用，因为它要求有具体的预期类型，而 Coe 类无法表达预期类型可以是任意宇宙。
当某个位置预期命题或类型，而在该位置精译出的项的推断类型并非命题或类型时，Lean 会尝试合成 CoeSort 实例来从错误中恢复。
如果找到了实例，且结果类型本身是一个类型，就会插入并展开该强制转换。
并非精译器期待宇宙的所有情形都需要 CoeSort。
在某些情况下，可以取得某个特定宇宙作为预期类型。
此时会使用 CoeT 进行普通的强制转换插入。
CoeSort 的实例可用于合成 CoeOut 实例，因此无需单独的实例来支持这种用法。
一般而言，强制转换为类型应实现为 CoeSort。
类型类
语法显式强制转换为 Sort
term ::= ...
|
可使用前缀运算符 ↥ 显式触发强制转换为 Sort。
Sort 强制转换
幺半群是配备了结合二元运算和单位元的类型。 幺半群结构可以定义为类型类，也可以定义为将结构与类型“捆绑”在一起的结构体：
structure Monoid where
Carrier : Type u
op : Carrier → Carrier → Carrier
id : Carrier
op_assoc :
∀ (x y z : Carrier), op x (op y z) = op (op x y) z
id_op_identity : ∀ (x : Carrier), op id x = x
op_id_identity : ∀ (x : Carrier), op x id = x
类型 Monoid 并不指明载体：
def StringMonoid : Monoid where
Carrier := String
op := (· ++ ·)
id := ""
op_assoc := ⊢ ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z x✝:Stringy✝:Stringz✝:String⊢ x✝ ++ (y✝ ++ z✝) = x✝ ++ y✝ ++ z✝; All goals completed! 🐙
id_op_identity := ⊢ ∀ (x : String), "" ++ x = x x✝:String⊢ "" ++ x✝ = x✝; All goals completed! 🐙
op_id_identity := ⊢ ∀ (x : String), x ++ "" = x x✝:String⊢ x✝ ++ "" = x✝; All goals completed! 🐙
不过，可以实现一个 CoeSort 实例：当幺半群出现在 Lean 期待类型的位置时，该实例应用 Monoid.Carrier 投影：
instance : CoeSort Monoid (Type u) where
coe m := m.Carrier
example : StringMonoid := "hello"
将 Sort 强制转换用作普通强制转换
归纳类型 NatOrBool 表示类型 Nat 和 Bool。
它的值可以强制转换为实际类型 Nat 和 Bool：
inductive NatOrBool where
| nat | bool
@[coe]
abbrev NatOrBool.asType : NatOrBool → Type
| .nat => Nat
| .bool => Bool
instance : CoeSort NatOrBool Type where
coe := NatOrBool.asType
open NatOrBool
当 nat 出现在冒号右侧时，会使用 CoeSort 实例：
def x : nat := 5
有预期类型时，会使用普通的强制转换插入。
在此例中，CoeSort 实例用于合成 CoeOut NatOrBool Type 实例；后者与 Coe Type (Option Type) 实例链接，以从类型错误中恢复。
def y : Option Type := bool