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

Revert "Moved explanation to DeBruijn#lookup"

Browse source 
This reverts commit dba3a4ae84.
This commit is contained in:
Wen Kokke 2019-09-18 16:20:03 +01:00
parent c0086ca017
commit ff882eccf6
1 changed files with 4 additions and 13 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,19 +420,10 @@ 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 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.
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).
Given the above, we can convert a natural to a corresponding
de Bruijn index, looking up its type in the context: