lean and latex

Stream: general

[Kevin Buzzard]

I want to be able to mix Lean code and math mode within a LaTeX document. I am writing calculations about Bernoulli numbers where everything happening in nat I want to be in lstlean and everything in $\mathbb{Q}$ I want to be in $\sum_{i+j=n}c_iB_i$ maths mode. Ultimately it means that I would like to have lstlean working in numerators of LaTeX \frac{<numerators>}{<denominators>}s and _{<subscripts>}. Or should I just use some kind of tt mode, \mathtt or something? I have no understanding of what is actually going on here but this sort of trick seems to be a kind of cool way of keeping a rational $/$ distinguished from a natural / and similarly for -.

[Kevin Buzzard]

badlatex.png

[Mario Carneiro]

I would just fake it using \mathtt and \color

[Kevin Buzzard]

better.png

[Kevin Buzzard]

maths mode eats the spaces in the lean

[Mario Carneiro]

\mbox{\texttt{...}} might help with that

[Mario Carneiro]

you might even be able to use lstlean in there, not sure

[Kevin Buzzard]

Nice --

$$\sum_{(i,j)\in\mbox{\lstinline{antidiagonal n}}}\frac{\mbox{\lstinline{pascal i j}}}{\mbox{\lstinline{j.succ}}}B_i = 1.$$

gives me
nice.png

[Kevin Buzzard]

The Lean font is a tiny bit too big compared to the maths font. The Lean n is bigger than the maths $(i,j)$.

[Rob Lewis]

At some point I modified my local lstlean.tex to scale things down slightly (in the whole document, not just math mode):

% Default style fors listingsred
lineskip={-1.5pt},
basicstyle={\ttfamily\scalefont{.95}},

You could probably make a macro for \mbox{\lstinline that passes a basicstyle that scales it down.

[Kevin Buzzard]

Can I get something like that in the docs? It's some theorem about Bernoulli numbers which I have in some branch of mathlib. I don't even know if it's the right way to document it, I've just been goofing around with writing some stuff up in LaTeX.

[Rob Lewis]

I think it's dangerous to use formatting tricks to convey semantic info in the docs. Even if the trick were used uniformly through all the doc pages, people showing up on a random page won't necessarily pick up on that. If there's something important to point out about the division maybe it's better to spell it out.

[Rob Lewis]

I don't object to the styling though.