Replaced 'De Bruijn' with 'de Bruijn'
This commit is contained in:
parent
32cab1f0c9
commit
5851f261eb
2 changed files with 2 additions and 2 deletions
|
@ -38,7 +38,7 @@ progress and preservation. Following chapters will look at a number
|
|||
of variants of lambda calculus.
|
||||
|
||||
Be aware that the approach we take here is _not_ our recommended
|
||||
approach to formalisation. Using De Bruijn indices and
|
||||
approach to formalisation. Using de Bruijn indices and
|
||||
inherently-typed terms, as we will do in
|
||||
Chapter [DeBruijn]({{ site.baseurl }}{% link out/plta/DeBruijn.md %}),
|
||||
leads to a more compact formulation. Nonetheless, we begin with named
|
||||
|
|
|
@ -251,7 +251,7 @@ init-last {Γ} γ = extensionality lemma
|
|||
lemma (S x) = refl
|
||||
\end{code}
|
||||
|
||||
The nth function takes a De Bruijn index and finds the corresponding
|
||||
The nth function takes a de Bruijn index and finds the corresponding
|
||||
value in the environment.
|
||||
|
||||
\begin{code}
|
||||
|
|
Loading…
Reference in a new issue