diff options
| author | David A. Madore <david+git@madore.org> | 2023-11-28 10:18:13 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2023-11-28 10:18:13 +0100 |
| commit | 4a9bd795283b80280fe40b8d54fd36eb72b22071 (patch) | |
| tree | f03f36e3744cde67a3be2cb5546f2555caf151d2 | |
| parent | 5d718f143bc8b11e257b1be3b2f42e4e5f5eb134 (diff) | |
| download | inf110-lfi-4a9bd795283b80280fe40b8d54fd36eb72b22071.tar.gz inf110-lfi-4a9bd795283b80280fe40b8d54fd36eb72b22071.tar.bz2 inf110-lfi-4a9bd795283b80280fe40b8d54fd36eb72b22071.zip | |
Alternative notation for multiple lambdas.
| -rw-r--r-- | transp-inf110-02-typage.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 7b1f031..d05ca00 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -855,8 +855,9 @@ $\sigma_1,\ldots,\sigma_k$ : \item « $\rho\to\sigma\to\tau$ » signifie « $(\rho\to(\sigma\to\tau))$ » ; « $xyz$ » signifie « $((xy)z)$ » ; -\item on note « $\lambda (x:\sigma,t:\tau).E$ » pour « $\lambda - (x:\sigma). \lambda (t:\tau). E$ » ; +\item {\footnotesize on note « $\lambda (x:\sigma,t:\tau).E$ » ou + « $\lambda (x:\sigma)(t:\tau).E$ » pour « $\lambda + (x:\sigma). \lambda (t:\tau). E$ » ;} \item l'abstraction est moins prioritaire que l'application ; \item on considère les termes à renommage près des variables liées {\footnotesize ($\alpha$-conversion)}. |