From f4a6f941a05fec83938e22da7a1c2b8a6803c5d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= <marko@dimjasevic.net>
Date: Fri, 2 Oct 2020 14:18:37 +0200
Subject: [PATCH] De Bruijn: Implements Wadler's feedback to PR #514

---
 src/plfa/part2/DeBruijn.lagda.md | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index d1158fe6..522f5457 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -451,9 +451,8 @@ We can then introduce a convenient abbreviation for variables:
    → Γ ⊢ lookup (toWitness n<?length)
 #_ n {n<?length}  =  ` count (toWitness n<?length)
 ```
-The type of function `#_` asks for clarification. Function `#_` takes
-an implicit argument `n<?length` that provides evidence for `n` to be
-within the context's bounds. Recall that
+Function `#_` takes an implicit argument `n<?length` that provides
+evidence for `n` to be within the context's bounds. Recall that
 [`True`]({{ site.baseurl }}/Decidable/#proof-by-reflection),
 [`_≤?_`]({{ site.baseurl }}/Decidable/#the-best-of-both-worlds) and
 [`toWitness`]({{ site.baseurl }}/Decidable/#decidables-from-booleans-and-booleans-from-decidables)