奉勸

睡前不要想問題 XD。

剛剛在床上把 relational derivation in Agda 想了一遍，應該是可行的，只是不知道實際寫起來會不會太複雜（proof terms 都是 functions）。最後的難關說不定就是「讓寫出來的形式能夠好看一點」。

幸好（？）現在 ghc 裝不起來，所以待會沒理由不睡 XD。不過上完作業系統回來，我應該就要馬上灌 OS X Tiger 到外接硬碟裡，把 ghc 以至 Agda 互動環境全部裝起來，然後試寫一點東西。安裝時間會非常長，不過看來沒別的選擇 — 開始心癢難搔了 XD。

--
而且也不能痴等 MacPorts 更新 XD。

---

然後再奉勸：要毅然決然地離開電腦。我現在準備要灌 Tiger 了 XD。

---

現在正在灌 MacPorts，待會讓 ghc 自己裝，我就可以睡了 XD。

---

如果在 Tiger 下面把相關的 port 都裝好，然後複製到 Leopard，不知道這樣有沒有用？XD