From 74d87812974916ce07a002d0666f89bbca7d752d Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 13 Jul 2020 23:50:28 +0100 Subject: [PATCH] Fixed issue with EPUB. --- src/plfa/part1/Decidable.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index 43fa799c..a7799fbc 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -548,7 +548,7 @@ postulate #### Exercise `iff-erasure` (recommended) 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: ``` postulate @@ -564,7 +564,7 @@ postulate ## Proof by reflection {#proof-by-reflection} 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 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`