Zulip Chat Archive

Stream: new members

Topic: multiple names for a lemma


Michael Beeson (Oct 20 2020 at 07:14):

I already have lemma le_transitive. But in my paper it's Lemma 30. So I looked for it as lemma30 and did not find it.
Finally I found le_transitive. So now let's give it BOTH names so we can find it either way. OK I can do it like this:

lemma lemma30:  (κ μ  : M), κ  𝔽  μ  𝔽    𝔽  κ      μ  κ  μ := le_transitive M

But I wish I could leave out the long formula and just write

lemma lemma30:= le_transitive M

but that is illegal for some reason.

Johan Commelin (Oct 20 2020 at 07:15):

Could it be

\begin{lemma} \label{le_transitive}
  blabla
\end{lemma}

in your paper?

Johan Commelin (Oct 20 2020 at 07:15):

If you use a package like \usepackage{showkeys} then you will even see the latex labels in the margin of your PDF

Johan Commelin (Oct 20 2020 at 07:16):

Because if you insert a lemma before "Lemma 30", you'll have a lot of renaming to do, if you do it your way. So I would suggest trying to write that 30 in as few places as possible. Preferably nowhere at all.

Mario Carneiro (Oct 20 2020 at 07:17):

you can use alias for this

Mario Carneiro (Oct 20 2020 at 07:17):

or def foo := @bar

Mario Carneiro (Oct 20 2020 at 07:17):

even if bar is a theorem

Mario Carneiro (Oct 20 2020 at 07:18):

although the linter will yell at you

Michael Beeson (Oct 20 2020 at 07:18):

Aha! That would be VERY useful. The only reason I'm naming these lemmas with numbers in Lean is so I can work with the pdf on one monitor and the Lean file on the other monitor. Since sync is more or less dysfunctional in TeXShop I need to work with the pdf mostly. I've already had to insert a lemma a couple of times. It's obviously a wrong way to work,
but I'm almost done now with this paper.

Mario Carneiro (Oct 20 2020 at 07:19):

If you are writing a formalization paper, you should definitely put the lemma names in the paper like Johan says

Mario Carneiro (Oct 20 2020 at 07:19):

don't do it the other way around, putting those terrible latex names in the formalization

Johan Commelin (Oct 20 2020 at 07:20):

@Michael Beeson Even in your setup, where you want to look at the PDF, instead of the tex source, I think you should use {showkeys}

Mario Carneiro (Oct 20 2020 at 07:20):

well, Johan's using them as labels but I would put them also in the print, i.e. \begin{lemma}[(\texttt{le_transitive})] ...

Johan Commelin (Oct 20 2020 at 07:24):

Why not let a package do that for you?

Mario Carneiro (Oct 20 2020 at 07:24):

I have nothing against it, I've never used showkeys

Mario Carneiro (Oct 20 2020 at 07:25):

not sure about using the margin for this though, that's often off limits depending on the stylesheet / target venue

Johan Commelin (Oct 20 2020 at 07:27):

At least one of those packages that shows labels in print is pretty configurable. I always forget which one is which.

Mario Carneiro (Oct 20 2020 at 07:28):

also I don't know whether I would want this for all \labels in the file, since I use \label also for section references and those don't get a texttt gloss

Johan Commelin (Oct 20 2020 at 07:32):

Well, I love it that they also show up in the margin while I'm writing the text. For the final product, I agree that it would be good to have a more polished solution.


Last updated: Dec 20 2023 at 11:08 UTC