擠

期末壓力大，如果這時候有其他具吸引力的目標就完蛋了，因為會很自然地被推擠過去 XD。scm 老師和我都碰到 Agda 的 bug，今天一併回報給實作者。很快地接到實作者的回信說 bug 修好了，我就很快樂地證畢一個關鍵的小 lemma XD。現在會用 dotted patterns，證明就變得簡單很多，不需要再煩瑣地處理 equality proofs。以往能耐心在那裡弄那些 symmetry, transitivity, substitution, congruence 之類的，還真是有毅力 XD。

--
MPEG-1 decoder 因而進展緩慢 XD。