diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-10-29 12:08:49 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:09 +0100 |
| commit | 8f96f8194608c99ad8efa201c24b527dbc530537 (patch) | |
| tree | 231c139b2c48d0178597f1335a85c8e5f422bfcc /doc/refman/RefMan-cic.tex | |
| parent | 660725e70918366d9f07183ae76c5a6284f81cc9 (diff) | |
CLEANUP PROPOSITION: The removed paragraph is not essential for this chapter. That kind of information is more appropriate for Section 1.2.
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index b1becba3f..ed7889e48 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -178,15 +178,6 @@ More precisely the language of the {\em Calculus of Inductive %\item cofixpoint ... \end{enumerate} -\paragraph{Notations.} Application associates to the left such that -$(t\;t_1\;t_2\ldots t_n)$ represents $(\ldots ((t\;t_1)\;t_2)\ldots t_n)$. The -products and arrows associate to the right such that $\forall~x:A,B\ra C\ra -D$ represents $\forall~x:A,(B\ra (C\ra D))$. One uses sometimes -$\forall~x~y:A,B$ or -$\lb x~y:A\mto t$ to denote the abstraction or product of several variables -of the same type. The equivalent formulation is $\forall~x:A, \forall y:A,B$ or -$\lb x:A \mto \lb y:A \mto t$ - \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$ |