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

De Bruijn: Implements Wadler's feedback to PR #514

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

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

@ -451,9 +451,8 @@ We can then introduce a convenient abbreviation for variables:
→ Γ ⊢ lookup (toWitness n<?length) → Γ ⊢ lookup (toWitness n<?length)
#_ n {n<?length} = ` count (toWitness n<?length) #_ n {n<?length} = ` count (toWitness n<?length)
``` ```
The type of function `#_` asks for clarification. Function `#_` takes Function `#_` takes an implicit argument `n<?length` that provides
an implicit argument `n<?length` that provides evidence for `n` to be evidence for `n` to be within the context's bounds. Recall that
within the context's bounds. Recall that
[`True`]({{ site.baseurl }}/Decidable/#proof-by-reflection), [`True`]({{ site.baseurl }}/Decidable/#proof-by-reflection),
[`_≤?_`]({{ site.baseurl }}/Decidable/#the-best-of-both-worlds) and [`_≤?_`]({{ site.baseurl }}/Decidable/#the-best-of-both-worlds) and
[`toWitness`]({{ site.baseurl }}/Decidable/#decidables-from-booleans-and-booleans-from-decidables) [`toWitness`]({{ site.baseurl }}/Decidable/#decidables-from-booleans-and-booleans-from-decidables)