推論規則をレイアウトする bcprules.sty
今まで推論規則を書くときは proof.sty を使っていた.
\[ \infer[\mbox{\sc T-App}]{ \Gamma \vdash t_1\ t_2 : \tau_2 }{ \Gamma \vdash t_1 : \tau_1 \rightarrow \tau_2 & \Gamma \vdash t_2 : \tau_1 } \]
しかし,前提の部分が長すぎる場合にどう改行してよいのか不明で*1,
\[ \infer[\mbox{\sc T-VeryLong}]{ \Gamma \vdash \mbox{foo}\ t_1\ t_2 : \mbox{bar}\ \alpha\ \beta }{ \Gamma \vdash t_1 : \mbox{very-long-constructor}\ \alpha & \Gamma \vdash t_2 : \mbox{another-very-long-constructor}\ \beta & \mbox{have-very-long-property}(\alpha, \beta) } \]
とかが Overfull \hbox というメッセージと共に
となってしまう.
Benjamin C. Pierce 先生の bcprules.sty を最近知った.
http://www.cis.upenn.edu/~bcpierce/papers/index.shtml
\infrule[T-App]{ \Gamma \vdash t_1 : \tau_1 \rightarrow \tau_2 \andalso \Gamma \vdash t_2 : \tau_1 }{ \Gamma \vdash t_1\ t_2 : \tau_2 }
と書くと
のようにレイアウトされる.まさに TAPL のレイアウトだ.
bcprules.sty の場合,先程のように前提が長い例は
\infrule[T-VeryLong]{ \Gamma \vdash t_1 : \mbox{very-long-constructor}\ \alpha \andalso \Gamma \vdash t_2 : \mbox{another-very-long-constructor}\ \beta \andalso \mbox{have-very-long-property}(\alpha, \beta) }{ \Gamma \vdash \mbox{foo}\ t_1\ t_2 : \mbox{bar}\ \alpha\ \beta }
\infrule[T-VeryLong]{ \Gamma \vdash t_1 : \mbox{very-long-constructor}\ \alpha \andalso \Gamma \vdash t_2 : \mbox{another-very-long-constructor}\ \beta \\ \andalso \mbox{have-very-long-property}(\alpha, \beta) }{ \Gamma \vdash \mbox{foo}\ t_1\ t_2 : \mbox{bar}\ \alpha\ \beta }
*1:\vbox 作ってその中に行毎に \hbox 作ってその中に書く,という方法でそれっぽいことはできた