diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index db26568c5a..fe32cb7266 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -354,6 +354,7 @@ be derived from the following rules. well-typed without having $((\lb x:T\mto u)~t)$ well-typed (where $T$ is a type of $t$). This is because the value $t$ associated to $x$ may be used in a conversion rule (see Section~\ref{conv-rules}). +% QUESTION: I do not understand. How would that be possible? \section[Conversion rules]{Conversion rules\index{Conversion rules} \label{conv-rules}} |