ytakano/rust_zero

9.1.4 p242 図9.3 中の誤植

cutsea110 opened this issue · 3 comments

cutsea110 commented

9.1.4 p242 図9.3 中の誤植と思われる箇所の報告です。
T-Pair の前件にあるQ(T_1) Q(T_2) はそれぞれ Q(Γ_1) Q(Γ_2) と思われます。

cutsea110 commented

これは私の勘違いのようなので取り下げます。

cutsea110 commented

Reopen させてもらいます。
やはりここでの Q は型環境を取るもののように思いました。
(仮に型をとるのであれば p243 の T-Pair の型付けにおける Un(\emptyset) は Un(un bool) でなければならないはずなので)

  • 👀1
cutsea110 commented

やはり私の理解が間違っていたので Close します。
p243 は 空の型環境に対して T-Bool を使った導出が端折られていたのですね。