新琴

好久沒到琴房了，今天進去發現換了新琴，可惜我的技巧愈來愈差了 XD。

晚上都在寫 DCL final project proposal（pdf 所在網址應該很好猜 XD），昨天就沒寫到 blog XD。

Relational derivation 一些簡單的性質都可以很簡單地組合出證明，看來還是要涉及比較具體的 functions 才用得上 chain reasoning。可是想做 chain reasoning 的話，proof terms 都是 functions，而且還要做 pattern matching，這樣整個 derivation 的長相會變得有點怪，大概上一半都是 by f1、by f2、…，然後下一半以 where 開頭，把所有 functions 定義出來。找不到什麼好方法哩 XD。

--
我會用「哩」了 XD。