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

Moved explanation to DeBruijn#lookup

Browse source
This commit is contained in:
Wen Kokke 2019-09-17 15:34:18 +02:00
parent 598747b8e9
commit dba3a4ae84
1 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -420,10 +420,19 @@ lookup (Γ , _) (suc n) = lookup Γ n
lookup ∅ _ = ⊥-elim impossible
where postulate impossible : ⊥
```
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]({{ site.baseurl }}/Lambda/#impossible).
We intend to apply the function only when the natural is shorter than the length
of the context, which we indicate by postulating a term `impossible` of the
empty type `⊥`. If we use C-c C-n to normalise the term
lookup (∅ , `ℕ ⇒ `ℕ , `ℕ) 3
Agda will return an answer warning us that the impossible has occurred:
⊥-elim (plfa.part2.DeBruijn.impossible 1)
While postulating the impossible is a useful technique, it must be
used with care, since such postulation could allow us to provide
evidence of _any_ proposition whatsoever, regardless of its truth.
Given the above, we can convert a natural to a corresponding
de Bruijn index, looking up its type in the context: