今まで推論規則を書くときは 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 } \] と書くと のようにレイアウトされる． しかし…

LaTeX で BNF 的なものを書くときに，::= や | の記号をいいかんじに揃えたい．縦に並べるだけなら eqnarray 環境でやればいいかんじに揃う． \begin{eqnarray*} t &::=& x \\ &|& t + t \\ &|& t - t \\ &|& t \times t \\ &|& t \div t \\ \end{eqnarray*}…