From 4beb1ee596afaf4ab4ebea9a89bb3ade7bbbe13d Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 29 Oct 2015 17:32:36 +0100 Subject: COMMENT: question --- doc/refman/RefMan-cic.tex | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/refman') 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}} -- cgit v1.2.3