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

[Elias Castegren]

Hi!

Even though it also has capabilities for generating theorem prover code,
I mainly use Ott [1] for writing and generating nice-looking type rules
in LaTeX. Together with Jesse Tov’s ottalt package, it gives me rules which
are as pretty as I could hope for, and in the style that you’re asking for (I think
it is using mathpartir under the hood). Having syntax and grammar checking to
make sure that you’re not making silly mistakes is a nice bonus. I still typeset
grammars by hand though, as the ones produced by Ott tend to be a bit too
whitespace hungry.

If you don’t want to introduce an external tool to your workflow, you could look
at the code that Ott (with ottalt) generates and borrow the tricks you need.

Cheers

/Elias

[1] https://www.cl.cam.ac.uk/~pes20/ott/

27 nov. 2019 kl. 22:38 skrev Norman Ramsey <nr at cs.tufts.edu<mailto:nr at cs.tufts.edu>>:

[ 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