From 747998cd63028654a54aab6d5f65bccbecb08656 Mon Sep 17 00:00:00 2001 From: Matthias Gabriel Date: Thu, 13 Feb 2020 15:46:39 +0100 Subject: [PATCH] Remove strange line break Remove a strange line break in the middle of the formula. I guess the mark-down respects that line break because it's part of the formula. --- src/plfa/part1/Induction.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index e7466153..99ecb0a8 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -656,8 +656,8 @@ time we are concerned with judgments asserting associativity: Now, we apply the rules to all the judgments 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 +`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: