2009/03/26

新航線

今天上學途中想到,我遇到的 typecast 問題其實可以用 2-level with-matching 解掉 ─ 如果要把 t : T e 換成 t : T e' 而且已知 e≡e' : e ≡ e',那麼可以先用 withe≡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。

Labels:

<< 回到主頁