yforster / coqtheorem Goto Github PK

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.

Not sure why, but it appears cleverref doesn't know the labels of normal environments anymore. Probably you guys are nesting environments or something?

It should create dashes.

I think the problem is here:
{\newcommand{\coqitem}[1][]{\stepcounter{enumi}\item[{\coqlink[#1]{\labelenumi}}]}}
This should be \labelitemi (for the outermost environment, in case it is in an itemize). In fact, it's probably wrong to use always i too. No idea how to make it context-aware.

I had to comment out the line

% \let\c@theorem\relax

or else align* environments give off massive errors