diff options
| author | Matej Kosik | 2015-10-29 17:32:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:10 +0100 |
| commit | 4beb1ee596afaf4ab4ebea9a89bb3ade7bbbe13d (patch) | |
| tree | bee7c7b840b429a07d7cffb3fa4de6a14a8346b6 | |
| parent | e31bc1fc036969454a5577758444b91174209b5c (diff) | |
COMMENT: question
| -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}} |