From fd10b0d5a917b84a329dff57a3129707175eb289 Mon Sep 17 00:00:00 2001 From: Matthew Healy Date: Fri, 31 Jul 2020 16:04:16 +0200 Subject: [PATCH] Fix newline rendering in Decidable chapter --- 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 8649ed0c..57fb90c6 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -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. 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 -≤? m`. This provides us with evidence whether `n ≤ m` holds or not. We erase the +through what this means step-by-step. First, we run the decision procedure, +`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 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