Skip to content
Snippets Groups Projects
Commit f27d4f85 authored by Mallku Soldevila's avatar Mallku Soldevila
Browse files

Minor change in Contexts section

parent eb70d3fc
No related branches found
No related tags found
1 merge request!18Minor changes in rule distinct_elim, nary_elim, distinct_elim, and source code docu. in doc.tex
Pipeline #51828 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
spec/doc.tex
+ 2
− 1
View file @ f27d4f85
...@@ -555,7 +555,8 @@ Every context $\Gamma$ induces a capture-avoiding substitution ...@@ -555,7 +555,8 @@ Every context $\Gamma$ induces a capture-avoiding substitution
$\subst(\Gamma)$. If $\Gamma$ is the empty list, $\subst(\Gamma)$. If $\Gamma$ is the empty list,
$\subst(\Gamma)$ is the empty substitution, i.e, the $\subst(\Gamma)$ is the empty substitution, i.e, the
identity function. 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$: substitution for $x_n$:
\[ \[
\subst([c_1,\dots, c_{n-1}, x_n]) \subst([c_1,\dots, c_{n-1}, x_n])
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment