From 3ee374bb0d1fe7713165325a62cca9e62d63508f Mon Sep 17 00:00:00 2001 From: Juhana Laurinharju Date: Sun, 27 May 2018 21:41:23 +0300 Subject: [PATCH] Fix typo in an equation in quantifiers --- src/Quantifiers.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Quantifiers.lagda b/src/Quantifiers.lagda index f9a3c976..a2ab8072 100644 --- a/src/Quantifiers.lagda +++ b/src/Quantifiers.lagda @@ -291,7 +291,7 @@ substituting for `n`. - If the number is odd because it is the successor of an even number, then we apply the induction hypothesis to give a number `m` and evidence that `m * 2 ≡ n`. We return a pair consisting of `suc m` and -evidence that `1 + 2 * m = suc n`, which is immediate after +evidence that `1 + m * 2 ≡ suc n`, which is immediate after substituting for `n`. This completes the proof in the forward direction.