Proof tree

打 Martin-Löf 的 intuitionistic type theory 講義練習用右手按 shift，打到 bounded μ-operator 的時候有棵龐大的 proof tree。雖然 bussproofs 很好用，對著樹直覺地做 post-order traversal 就打完了，但整棵樹因為太寬立刻超出頁面。和原稿相比較，一些枝葉茂盛的 subtrees 應該延伸到旁邊比較小的 subtrees 上面，但 bussproofs 不會做這種最佳化，\insertBetweenHyps 對於三個前提的 inference 又沒辦法指定特定一個間隔插入 \hskip，於是乾脆直接改 bussproofs 的源碼，才把樹調得窄一點，但還是塞不進 \textwidth。最後只好手動調整，讓樹均勻超過左右邊界 XD。

--
不懂的源碼也照改，這就是資訊系的訓練？XD

Beamer 初體驗

昨天晚上本來只是想試試用 beamer 打個式子看效果如何，結果就上癮了，一打就打到三點 XD。試 beamer 主要是為了做賽局理論課程 paper 報告的投影片，現在只用寥寥數個指令，效果就已經讓我挺滿意了。有半成品可以下載 XD。

--
不過這樣勢必得面對中文問題…