diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index a97fce8700..f0046ffe6a 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -388,12 +388,13 @@ may be used in a conversion rule (see Section~\ref{conv-rules}). \section[Conversion rules]{Conversion rules\index{Conversion rules} \label{conv-rules}} -\paragraph[$\beta$-reduction.]{$\beta$-reduction.\label{beta}\index{beta-reduction@$\beta$-reduction}} In \CIC, there is an internal reduction mechanism. In particular, it can decide if two programs are {\em intentionally} equal (one says {\em convertible}). Convertibility is described in this section. +\paragraph[$\beta$-reduction.]{$\beta$-reduction.\label{beta}\index{beta-reduction@$\beta$-reduction}} + We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For instance the identity function over a given type $T$ can be written |