15_2.txt

# 15.5.1

（保存） t:Tで t -> t' のとき、t':T

証明のとっかかりが分からない……


# 15.5.2

(1)

T1 <: S1
------------------
Ref S1 <: Ref T1

T1: {a:Nat,b:Truth}
S1: {a:Nat}
として以下を実行する。

```
r = ref {a: 5}
>> r : Ref S1

// Ref S1 <: Ref T1 であるため、↓が可能

f = (\x:Ref T1. x!)
u: T1 = f r
>> u : T1 (値は{a:5})
```

このuをT1の文脈で使用（e.g. u.bを利用）すると、評価が行き詰まってしまう。


(2)

S1 <: T1
------------------
Ref S1 <: Ref T1

S1: {a:Nat,b:Truth}
T1: {a:Nat}
として以下を実行する。

```
r = ref {a: 5, b: 42}
>> r : Ref S1

// Ref S1 <: Ref T1 であるため、↓が可能

f = (\x:Ref T1. x := {a:5})
f r
>> rの値は{a:5}:T1になる

u: S1 = !r
```

このuをT1の文脈で使用（e.g. u.bを利用）すると、評価が行き詰まってしまう。


# 15.5.3

配列だと長さが違うものを代入した結果落ちる、とかありそう（こなみ）