From 6ec9eea5c8d3eeae6d20d35c6f3c583f5a994147 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 24 Jan 2019 21:07:03 +0100 Subject: [PATCH] Decidables: adds a word fix to a version under extra --- extra/extra/DecidableExtra.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extra/extra/DecidableExtra.lagda b/extra/extra/DecidableExtra.lagda index b2ee3094..45d17417 100644 --- a/extra/extra/DecidableExtra.lagda +++ b/extra/extra/DecidableExtra.lagda @@ -193,7 +193,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.