diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 229c01b5d..764f1189b 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -349,7 +349,14 @@ be derived from the following rules. \inference{\frac{\WTEG{t}{T}~~~~ \WTE{\Gamma::(x:=t:T)}{u}{U}} {\WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}}} \end{description} - + +\Rem Prod$_1$ and Prod$_2$ typing-rules make sense if we consider the semantic +difference between {\Prop} and {\Set}: +\begin{itemize} + \item All values of a type that has a sort {\Set} are extractable. + \item No values of a type that has a sort {\Prop} are extractable. +\end{itemize} + \Rem We may have $\kw{let}~x:=t:T~\kw{in}~u$ 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$ |