Lists: adds colons before code snippets #2

Agda-zh · Mar 12, 2019 · 17f8a16 · 17f8a16
1 parent 3c71a27
commit 17f8a16
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/plfa/Lists.lagda b/src/plfa/Lists.lagda
@@ -177,11 +177,11 @@ inductive hypothesis.  As usual, the inductive hypothesis is indicated by a recu
 invocation of the proof, in this case `++-assoc xs ys zs`.
 
 Recall that Agda supports [sections][plfa.Induction#sections].
-Applying `cong (x ∷_)` promotes the inductive hypothesis
+Applying `cong (x ∷_)` promotes the inductive hypothesis:
 
     xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
 
-to the equality
+to the equality:
 
     x ∷ (xs ++ (ys ++ zs)) ≡ x ∷ ((xs ++ ys) ++ zs)