CoeSort の説明に誤り

[Seasawher]

Coe とどう違うのかの説明が間違っている。現状の説明では、「型宇宙へ」強制する場合には CoeSort でないといけないかのように見えるが、以下のように Coe で型宇宙への強制を行うことができる。

Coe と CoeSort の違いは、「強制のトリガーがどこにあるのか」で説明すべき。

def zero (α : Type) : Nat := 0

/-- `Type` のラッパー -/
structure AltType where
  base : Type

def A : AltType := ⟨Nat⟩

/--
error: application type mismatch
  zero A
argument
  A
has type
  AltType : Type 1
but is expected to have type
  Type : Type 1
-/
#guard_msgs in #eval zero A

instance : Coe AltType Type := ⟨fun S ↦ S.base⟩

-- ちゃんと評価できる
#eval zero A