Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

\coqitem doesn't support \labels #2

Open
ghost opened this issue Aug 14, 2018 · 0 comments
Open

\coqitem doesn't support \labels #2

ghost opened this issue Aug 14, 2018 · 0 comments

Comments

@ghost
Copy link

ghost commented Aug 14, 2018

I have a "meta"-lemma, where I actually enumerate coq-lemmas:

\begin{lemma}[Name of the lemma]
\label{lem:metalemma}~
\begin{enumerate}
\item \label{lem:lem1} bli
\item \label{lem:lem2} bla
\item \label{lem:lem3} blub
\end{enumerate}
\end{lemma}

In the proof, I refer to the items as "claims":

\begin{proof}
Claim~\ref{lem:lem1} follows by induction.  Claim~\ref{lem:lem2} is trivial.  Claim~\ref{lem:lem3} follows with claims~\ref{lem:lem1} and~\ref{lem:lem2}
\end{proof}

If I refer to (sub) lemma 1 somwhere, I use see Lemma~\ref{lem:metalemma}~(\ref{lem:lem1}).

This works as expected. However, if I replace \item with \coqitem[...], this doesn't work any more.
The reason for that is that, is that \item[name] doesn't support labels.

My work-around was to \coqlink the descriptions (\coqlink[...]{bli}), but there should be a more elegant solution.

See also this question on tex.sx for a possible solution to this problem. The accepted solution does what I would expect. It shouldn't be that hard to implement this for coqtheorem.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

0 participants