diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-23 17:56:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:06 +0100 |
| commit | f1f19693f16a914b167ebcb18e96aac25a582920 (patch) | |
| tree | d340705cb99cc5d0b748e1f52a5040289776c8cd /doc/refman/RefMan-cic.tex | |
| parent | 08857b1f4455e942aeba456affdb0f61eaa4266a (diff) | |
fix
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -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 a97fce870..f0046ffe6 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 |