From ecec10e84001cb861976140fbf2381c0a547a8b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 24 Oct 2020 17:00:27 +0200 Subject: [PATCH] DeBruijn: refresh a function description given its new implementation (#542) --- src/plfa/part2/DeBruijn.lagda.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index bd3e8b60..9b94d5ff 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -428,10 +428,8 @@ lookup {(_ , A)} {zero} (s≤s z≤n) = A lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p ``` -We intend to apply the function only when the natural is -shorter than the length of the context, which we indicate by -postulating an `impossible` term, just as we did -[here](/Lambda/#primed). +We intend to apply the function only when the natural is shorter than +the length of the context, which is witnessed by `p`. Given the above, we can convert a natural to a corresponding de Bruijn index, looking up its type in the context: