yforster / coqtheorem Goto Github PK

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.

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

I had to comment out the line

% \let\c@theorem\relax

or else align* environments give off massive errors

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.