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

[Peter Sewell]

The default Ott style using Rok Strnisa and Matt Parkinson's ottlayout.sty
(in the Ott distro) also does what you want, as far as I can see - the
plain default puts rules one-per-line, while ottlayout lets one choose
whether to do that or just lay rules out like words in text (and also lets
one control many other things).   The \fbox'd judgement is just slapped
down as a line or as the first thing, respectively.

Peter



On Thu, 28 Nov 2019 at 08:12, Elias Castegren <eliasca at kth.se> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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
>
>
>