Zulip Chat Archive

Stream: general

Topic: lean and latex


Kevin Buzzard (Dec 26 2020 at 18:40):

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 Q\mathbb{Q} I want to be in i+j=nciBi\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 (Dec 26 2020 at 18:40):

badlatex.png

Mario Carneiro (Dec 26 2020 at 18:41):

I would just fake it using \mathtt and \color

Kevin Buzzard (Dec 26 2020 at 18:45):

better.png

Kevin Buzzard (Dec 26 2020 at 18:46):

maths mode eats the spaces in the lean

Mario Carneiro (Dec 26 2020 at 18:47):

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

Mario Carneiro (Dec 26 2020 at 18:48):

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

Kevin Buzzard (Dec 26 2020 at 18:53):

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 (Dec 26 2020 at 18:55):

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

Rob Lewis (Dec 26 2020 at 19:00):

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 (Dec 26 2020 at 19:01):

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 (Dec 26 2020 at 19:07):

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 (Dec 26 2020 at 19:08):

I don't object to the styling though.


Last updated: Dec 20 2023 at 11:08 UTC