diff options
| author | Matej Kosik | 2015-10-29 13:47:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:09 +0100 |
| commit | 1372e075c52aa2dad547a42eaf9aba1f83a7abb1 (patch) | |
| tree | 3e0e25a83d4e012fcf236b3d323ce6e9ec650f90 | |
| parent | 8f96f8194608c99ad8efa201c24b527dbc530537 (diff) | |
CLEANUP PROPOSITION: this sentence does not help us to better understand the semantics of the language
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index ed7889e480..fb6a5bff83 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -181,8 +181,7 @@ More precisely the language of the {\em Calculus of Inductive \paragraph{Free variables.} The notion of free variables is defined as usual. In the expressions $\lb x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$ -are bound. They are represented by de Bruijn indexes in the internal -structure of terms. +are bound. \paragraph[Substitution.]{Substitution.\index{Substitution}} The notion of substituting a term $t$ to free occurrences of a |