From 3ef2ee4bedcf5620b5a8368f443a8cc4d4e4e2bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 24 Jan 2019 20:56:12 +0100 Subject: [PATCH] Decidable: fixes the spelling of a word --- src/plfa/Decidable.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Decidable.lagda b/src/plfa/Decidable.lagda index a1dcd7e0..c10015a1 100644 --- a/src/plfa/Decidable.lagda +++ b/src/plfa/Decidable.lagda @@ -200,7 +200,7 @@ The forward proof has one more clause than the reverse proof, precisely because in the forward proof we need clauses corresponding to the comparison yielding both true and false, while in the reverse proof we only need clauses corresponding to the case where there is evidence -that the comparision holds. This is exactly why we tend to prefer the +that the comparison holds. This is exactly why we tend to prefer the evidence formulation to the computation formulation, because it allows us to do less work: we consider only cases where the relation holds, and can ignore those where it does not.