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

Fix newline rendering in Decidable chapter

Browse source
This commit is contained in:
Matthew Healy 2020-07-31 16:04:16 +02:00
parent 6a2f296e32
commit fd10b0d5a9
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

@ -595,8 +595,8 @@ fill in an implicit of an *empty* record type, since there aren't any fields
after all. This is why `⊤` is defined as an empty record. after all. This is why `⊤` is defined as an empty record.
The trick is to have an implicit argument of the type `T ⌊ n ≤? m ⌋`. Let's go The trick is to have an implicit argument of the type `T ⌊ n ≤? m ⌋`. Let's go
through what this means step-by-step. First, we run the decision procedure, `n through what this means step-by-step. First, we run the decision procedure,
≤? m`. This provides us with evidence whether `n ≤ m` holds or not. We erase the `n ≤? m`. This provides us with evidence whether `n ≤ m` holds or not. We erase the
evidence to a boolean. Finally, we apply `T`. Recall that `T` maps booleans into evidence to a boolean. Finally, we apply `T`. Recall that `T` maps booleans into
the world of evidence: `true` becomes the unit type `⊤`, and `false` becomes the the world of evidence: `true` becomes the unit type `⊤`, and `false` becomes the
empty type `⊥`. Operationally, an implicit argument of this type works as a empty type `⊥`. Operationally, an implicit argument of this type works as a