From 5851f261ebbbdba8da73eadc4711c754867f36ae Mon Sep 17 00:00:00 2001 From: Reza Gharibi Date: Sat, 15 Jun 2019 20:59:07 +0430 Subject: [PATCH] Replaced 'De Bruijn' with 'de Bruijn' --- extra/extra/Lambda-new.lagda | 2 +- src/plfa/Denotational.lagda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/extra/extra/Lambda-new.lagda b/extra/extra/Lambda-new.lagda index 3d5c98ab..9a9e0770 100644 --- a/extra/extra/Lambda-new.lagda +++ b/extra/extra/Lambda-new.lagda @@ -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 diff --git a/src/plfa/Denotational.lagda b/src/plfa/Denotational.lagda index aa1ff205..13eeca46 100644 --- a/src/plfa/Denotational.lagda +++ b/src/plfa/Denotational.lagda @@ -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}