From f27d4f853a964e74f2211164101934be4f979635 Mon Sep 17 00:00:00 2001 From: Mallku2 <mallkuernesto@gmail.com> Date: Thu, 13 Feb 2025 20:59:41 -0300 Subject: [PATCH] Minor change in Contexts section --- spec/doc.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/spec/doc.tex b/spec/doc.tex index d16a68b..6505e3f 100644 --- a/spec/doc.tex +++ b/spec/doc.tex @@ -555,7 +555,8 @@ Every context $\Gamma$ induces a capture-avoiding substitution $\subst(\Gamma)$. If $\Gamma$ is the empty list, $\subst(\Gamma)$ is the empty substitution, i.e, the identity function. -The first case fixes $x_n$ and allows the context to shadow a previously defined +Otherwise, if $\Gamma$ ends with variable $x_n$, this fixes the variable +and allows the context to shadow a previously defined substitution for $x_n$: \[ \subst([c_1,\dots, c_{n-1}, x_n]) -- GitLab