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

Fixed issue with EPUB.

Browse source
This commit is contained in:
Wen Kokke 2020-07-13 23:50:28 +01:00
parent c56db8000d
commit 74d8781297
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part1/Decidable.lagda.md
View file

@ -548,7 +548,7 @@ postulate
#### Exercise `iff-erasure` (recommended) #### Exercise `iff-erasure` (recommended)
Give analogues of the `_⇔_` operation from Give analogues of the `_⇔_` operation from
Chapter [Isomorphism]({{ site.baseurl}}/Isomorphism/#iff), Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff),
operation on booleans and decidables, and also show the corresponding erasure: operation on booleans and decidables, and also show the corresponding erasure:
``` ```
postulate postulate
@ -564,7 +564,7 @@ postulate
## Proof by reflection {#proof-by-reflection} ## Proof by reflection {#proof-by-reflection}
Let's revisit our definition of monus from Let's revisit our definition of monus from
Chapter [Naturals]({{ site.baseurl}}/Naturals/). Chapter [Naturals]({{ site.baseurl }}/Naturals/).
If we subtract a larger number from a smaller number, we take the result to be If we subtract a larger number from a smaller number, we take the result to be
zero. We had to do something, after all. What could we have done differently? We zero. We had to do something, after all. What could we have done differently? We
could have defined a *guarded* version of minus, a function which subtracts `n` could have defined a *guarded* version of minus, a function which subtracts `n`