新航線

今天上學途中想到，我遇到的 typecast 問題其實可以用 2-level with-matching 解掉 ─ 如果要把 t : T e 換成 t : T e' 而且已知 e≡e' : e ≡ e'，那麼可以先用 with 把 e≡e' 放進 context 裡，接著對 e 做第二次 with-match 使 context 裡面的 e 都代換成一個單純的 pattern variable，同時讓 e≡e' 匹配成 refl 使那個 pattern variable 強制配為 e'，此時 t 的 type 就改成 T e' 了。這是很久以前 scm 老師在 Agda mailing list 上問到的手法，今天我又重新發明了一次 XD。過了這關之後，又發現我的 encoding 有點麻煩，今天再改改看。

今天晚上吃完台大牛肉麵，繞經學校北緣人行道穿進辛亥路側門，擦過系館和博理館回到宿舍區，速度 warp 3 只花 15 分鐘。只是這條新航線會經過天文數學館的工地，稍微不安全一點 XD。

今日飲食：中午紅燒牛肉燴飯 + 檸檬汁 @ 7-11（$65）；晚上牛肉湯麵 + 燙青菜 @ 台大牛肉麵（$100）+ 巧克力葡萄奶酥 @ 男一麵包店（$18）+ 蘋果汁 @ 男七販賣機（$13）。合計 $196。

--
大家都只對棒球有興趣 XD。