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

De Bruijn: implement feedback to PR #514 by Wadler and Kokke

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-01 22:33:59 +02:00
parent ef3b3b00aa
commit a889fa0273
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -451,13 +451,16 @@ 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. The function takes
an implicit argument `n<?length` that signals if there is evidence for
`n` to be within the context's bounds. Both `True` and `_≤?_` are
defined in Chapter [Decidable]({{ site.baseurl }}/Decidable/). The type
of `n<?length` guards against invoking `#_` on an `n` that is out of
context bounds. Finally, in the return type `n<?length` is converted
to a witness that `n` is within the bounds.
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
[`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)
are defined in Chapter [Decidable]({{ site.baseurl }}/Decidable/). The
type of `n<?length` guards against invoking `#_` on an `n` that is out
of context bounds. Finally, in the return type `n<?length` is
converted to a witness that `n` is within the bounds.
With this abbreviation, we can rewrite the Church numeral two more compactly:
```