LEAN code listing

Stream: new members

[Rohan Joshi]

Hi everyone! I wanted to create a project with LEAN code. However, when using Overleaf and I use listing, some of the mathematical symbols do not appear, such as the not equal symbol, integer symbol. Is there any way I can fix this? Thanks

[mars0i]

I don't use Overleaf, but I'm very familiar with LaTeX. I'm not sure whether I understand what you're asking.

Maybe you're saying that when you use the Unicode characters "≠" or "ℤ" they don't show up in Overleaf? If so, then in theory, by specification of the right font in LaTeX, I think you could make this work, but there's a better way, I think.

Apologies if you already know this: Mathematical characters are usually specified in LaTeX using special LaTeX strings in math mode, which can be specified by placing the special strings between "$" and "$" (to make the math symbols to appear within a longer line of text).

So for example, you would write "ℕ ≠ ℤ" in LaTeX as "$\mathbb{N} \neq \mathbb{Z}$". ("\mathbb" stands for "math blackboard bold", a name for the kind of font the natural number and integer symbols use.)

So I think that you just have to embed the math symbols in your code listing using this traditional LaTeX technique.

There are web pages that list the available LaTeX math symbols. Here's one at the Overleaf site:
https://www.overleaf.com/learn/latex/List_of_Greek_letters_and_math_symbols
If that page lacks a math character you need, searching for "latex math symbols" on the web will bring up other pages with other symbols.

On the other hand: Lean uses some symbols that look similar to each other. So for example, the usual right-arrow code in LaTeX, "\rightarrow", might not produce an exact equivalent of the Unicode "→" symbol used to specify Lean function types. Lean uses other arrows for other purposes. There are other arrows you can use in LaTeX too, but if it's important to have the exact Unicode character in your code listing, you might have to do more investigation or find a font that will allow LaTeX to render the Unicode characters you need.

(One possible drawback is that I think the font the math symbols are in might not be a perfect fit with the font used for code listings. You should be able to adjust these fonts by adding specifications of the fonts for math and for code listings, but that's kind of a pain to figure out, so hopefully the default fonts will look good enough together for your purposes.)

[Eric Wieser]

I don't think the above is good advice. You should not be modifying your lean code to use latex commands, you should be modifying your latex configuration to work with lean code.

[mars0i]

Rohan, to follow Eric's advice, you may have to do a bit of experimentation with different fonts--not sure. Regardless, this page seems relevant to your situation: https://www.overleaf.com/learn/latex/Articles/Unicode%2C_UTF-8_and_multilingual_text%3A_An_introduction
You might also find it helpful to search and ask questions on the TeX/LaTeX Stackoverflow site: https://tex.stackexchange.com/

[Eric Wieser]

A quick route to success is LuaLaTeX (select in the overleaf settings) + JuliaMono (upload to overleaf and configure with fontspec) + minted

[Bolton Bailey]

I think someone should perhaps provide this link to the lean FRO approved style file

https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex

[Eric Wieser]

Note there is no such fro-approved style file for minted because it works out of the box

[Eric Wieser]

So really, we should link to https://lean-lang.org/lean4/doc/syntax_highlight_in_latex.html