[TYPES] seeking stupid LaTeX tricks for laying out sets of typing rules

[Gabriel Scherer]

My approach is to put the judgment-declaration box on its own line, where
it ends up centered. With mathpartir (
http://cristal.inria.fr/~remy/latex/mathpartir.html ), a blank line acts as
a "normal separation" between elements (which are fit automatically on
lines), while \\ forces a break, so I would use

\begin{mathpar}
  \fbox{judgment1}~\text{explanation}
  \\
  rule1

  rule2

  rule3
\\
  \fbox{judgment2}~text{explanation}
  \\
  rule1

  rule2
  [...]
\end{mathpar}

On some occasions where I wanted to left-align or right-align an object on
a mathpar line, I have used unbreakable spaces as "fake" elements to
consume space (note: \and is equivalent ot a newline):

\\
  left-aligned object

  ~\and~\and~\and~\and~

  right-aligned object
\\

It's a very ugly hack, and it works reasonably well.

On Thu, Nov 28, 2019 at 6:50 AM Norman Ramsey <nr at cs.tufts.edu> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear Colleagues,
>
> I'm looking for advice on preparing figures full of typing rules.
> What I'd like is to create a figure that has a boxed form of judgment
> in the top left, then collects all the rules that can prove judgments
> of the boxed form.
>
> At present, I'm using Didier Rémy's mathpartir package.
> The inference rules are nice and readable, and I can collect them
> easily enough in a `mathpar` environment.  But the boxed judgment is
> placed as if it were just another rule, where it really ought to be in
> the upper left corner (or some other location which can indicate that
> it classifies all the rules).  I'm sure there must be a trick, but I
> haven't yet discovered it.
>
> How are you typesetting collections of inference rules?
>
>
> Norman
>
>