diff options
Diffstat (limited to 'doc')
| -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 b1becba3f5..ed7889e480 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$ |