Adds a missing closing parenthesis

This commit is contained in:
Marko Dimjašević 2020-09-25 12:18:56 +02:00
parent edcf159ea9
commit ef3b3b00aa
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA

View file

@ -454,7 +454,7 @@ We can then introduce a convenient abbreviation for variables:
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
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.