File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -548,7 +548,7 @@ postulate
548548#### Exercise ` iff-erasure ` (recommended)
549549
550550Give analogues of the ` _⇔_ ` operation from
551- Chapter [ Isomorphism] ({{ site.baseurl}}/Isomorphism/#iff),
551+ Chapter [ Isomorphism] ({{ site.baseurl }}/Isomorphism/#iff),
552552operation on booleans and decidables, and also show the corresponding erasure:
553553```
554554postulate
@@ -564,7 +564,7 @@ postulate
564564## Proof by reflection {#proof-by-reflection}
565565
566566Let's revisit our definition of monus from
567- Chapter [ Naturals] ({{ site.baseurl}}/Naturals/).
567+ Chapter [ Naturals] ({{ site.baseurl }}/Naturals/).
568568If we subtract a larger number from a smaller number, we take the result to be
569569zero. We had to do something, after all. What could we have done differently? We
570570could have defined a * guarded* version of minus, a function which subtracts ` n `
You can’t perform that action at this time.
0 commit comments