推論規則をレイアウトする bcprules.sty

Wed January 11, 2012

■[LaTeX] 推論規則をレイアウトする 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
}