michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

DeBruijn: refresh a function description given its new implementation (#542)

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-24 17:00:27 +02:00 committed by GitHub
parent 5326f16a8b
commit ecec10e840
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/plfa/part2/DeBruijn.lagda.md
View file

@ -428,10 +428,8 @@ lookup {(_ , A)} {zero} (s≤s z≤n) = A
lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p
``` ```
We intend to apply the function only when the natural is We intend to apply the function only when the natural is shorter than
shorter than the length of the context, which we indicate by the length of the context, which is witnessed by `p`.
postulating an `impossible` term, just as we did
[here](/Lambda/#primed).
Given the above, we can convert a natural to a corresponding Given the above, we can convert a natural to a corresponding
de Bruijn index, looking up its type in the context: de Bruijn index, looking up its type in the context: