From e42aa017dac06a10b319e00be04681393c22b8e4 Mon Sep 17 00:00:00 2001 From: Jonathan Prieto-Cubides Date: Fri, 6 Jul 2018 00:11:44 +0200 Subject: [PATCH 1/2] [ Induction ] Fix typo of of typo --- src/plfa/Induction.lagda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/Induction.lagda b/src/plfa/Induction.lagda index a678a0fc..c450df23 100644 --- a/src/plfa/Induction.lagda +++ b/src/plfa/Induction.lagda @@ -314,7 +314,7 @@ For the base case, we must show: zero + zero ≡ zero -Simplifying with the base case of of addition, this is straightforward. +Simplifying with the base case of addition, this is straightforward. For the inductive case, we must show: @@ -385,7 +385,7 @@ For the base case, we must show: zero + suc n ≡ suc (zero + n) -Simplifying with the base case of of addition, this is straightforward. +Simplifying with the base case of addition, this is straightforward. For the inductive case, we must show: From 504b194db22f8d945c85a6c9b319156d04a34c8f Mon Sep 17 00:00:00 2001 From: Jonathan Prieto-Cubides Date: Fri, 6 Jul 2018 00:43:04 +0200 Subject: [PATCH 2/2] Fix break verbatim --- src/plfa/Induction.lagda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/plfa/Induction.lagda b/src/plfa/Induction.lagda index c450df23..91389c36 100644 --- a/src/plfa/Induction.lagda +++ b/src/plfa/Induction.lagda @@ -497,9 +497,10 @@ time we are concerned with judgements asserting associativity. Now, we apply the rules to all the judgements we know about. The base case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural `n` and `p`. The inductive case tells us that if `(m + n) + p ≡ m + -(n + p)` (on the day before today) then `(suc m + n) + p ≡ suc m + (n -+ p)` (today). We didn't know any judgments about associativity -before today, so that rule doesn't give us any new judgments. +(n + p)` (on the day before today) then +`(suc m + n) + p ≡ suc m + (n + p)` (today). +We didn't know any judgments about associativity before today, so that +rule doesn't give us any new judgments. -- on the first day, we know about associativity of 0 (0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...