Zulip Chat Archive

Stream: general

Topic: lean and latex


view this post on Zulip 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 -.

view this post on Zulip Kevin Buzzard (Dec 26 2020 at 18:40):

badlatex.png

view this post on Zulip Mario Carneiro (Dec 26 2020 at 18:41):

I would just fake it using \mathtt and \color

view this post on Zulip Kevin Buzzard (Dec 26 2020 at 18:45):

better.png

view this post on Zulip Kevin Buzzard (Dec 26 2020 at 18:46):

maths mode eats the spaces in the lean

view this post on Zulip Mario Carneiro (Dec 26 2020 at 18:47):

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

view this post on Zulip Mario Carneiro (Dec 26 2020 at 18:48):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 26 2020 at 19:08):

I don't object to the styling though.


Last updated: May 17 2021 at 21:12 UTC