Zulip Chat Archive

Stream: general

Topic: lstlean.tex typos?

Peter Jipsen (Jun 15 2020 at 21:58):

I'm using https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.tex and noticed an issue with the following 4 lines


It seems they should be replaced by


I'm not sure if this should be raised as an issue on github.

Kevin Buzzard (Jun 15 2020 at 22:02):

This looks good to me -- you could just fix them with a PR if it's as easy as making an issue.

Kevin Buzzard (Jun 15 2020 at 22:07):

wait -- is \nsubset a thing in LaTeX?

Peter Jipsen (Jun 15 2020 at 22:29):

Yes, thanks, using \nsubset or \nsupset gives an error on my texlive distribution, so I'll put in a PR with


(\nsubseteq and \nsupseteq work for me, so I'm not editing those lines, but I hope someone will check this).

Kevin Buzzard (Jun 15 2020 at 23:26):

yes, \nsubseteq works for me in LaTeX but not \nsubset

Last updated: Dec 20 2023 at 11:08 UTC