2009/01/14

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

Labels:

Blogger yen31/14/2009 5:27 pm 說:

不懂的源碼改到對才是資訊系的訓練XD

 
Blogger Unknown1/15/2009 11:00 am 說:

natural deduction 的符號是要怎麼打啊, 用 \frac ?

 
Blogger Josh Ko1/15/2009 12:25 pm 說:

我是用 bussproofs 這個 package,還滿方便的。

不知不覺我已經打到 wellorderings,快打完整份了 XD。

 

<< 回到主頁