lstlean.tex typos?

Stream: general

[Peter Jipsen]

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

{⊂}{{\color{symbolcolor}\ensuremath{\subseteq}}}1
{⊄}{{\color{symbolcolor}\ensuremath{\nsubseteq}}}1
{⊃}{{\color{symbolcolor}\ensuremath{\supseteq}}}1
{⊅}{{\color{symbolcolor}\ensuremath{\nsupseteq}}}1

It seems they should be replaced by

{⊂}{{\color{symbolcolor}\ensuremath{\subset}}}1
{⊄}{{\color{symbolcolor}\ensuremath{\nsubset}}}1
{⊃}{{\color{symbolcolor}\ensuremath{\supset}}}1
{⊅}{{\color{symbolcolor}\ensuremath{\nsupset}}}1

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

[Kevin Buzzard]

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

[Kevin Buzzard]

wait -- is \nsubset a thing in LaTeX?

[Peter Jipsen]

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

{⊂}{{\color{symbolcolor}\ensuremath{\subset}}}1
{⊄}{{\color{symbolcolor}\ensuremath{\not\subset}}}1
{⊃}{{\color{symbolcolor}\ensuremath{\supset}}}1
{⊅}{{\color{symbolcolor}\ensuremath{\not\supset}}}1

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

[Kevin Buzzard]

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