fix typos

Author: Alex Gryzlov

src/Induction.lidr

@@ -285,7 +285,7 @@ $\square$
 The `replace` tactic allows you to specify a particular subterm to rewrite and
 what you want it rewritten to: `replace (t) with (u)` replaces (all copies of)
 expression `t` in the goal by expression `u`, and generates `t = u` as an
-additional subgoal. This is often useful when a plain \idr{rewrite` acts on the
+additional subgoal. This is often useful when a plain \idr{rewrite} acts on the
 wrong part of the goal.
 
 Use the `replace` tactic to do a proof of \idr{plus_swap'}, just like

src/Lists.lidr

@@ -486,7 +486,7 @@ this fact directly gives rise to a way of reasoning about inductively defined
 sets: a number is either \idr{Z} or else it is \idr{S} applied to some _smaller_
 number; a list is either \idr{Nil} or else it is \idr{Cons} applied to some
 number and some _smaller_ list; etc. So, if we have in mind some proposition
-\idr{p} that mentions a list \idr{l} and we want to argue that \idr{P} holds for
+\idr{p} that mentions a list \idr{l} and we want to argue that \idr{p} holds for
 _all_ lists, we can reason as follows:
 
   - First, show that \idr{p} is true of \idr{l} when \idr{l} is \idr{Nil}.
@@ -527,7 +527,7 @@ _Proof_: By induction on \idr{l1}.
 
   - First, suppose \idr{l1 = []}. We must show
 
-    \idr{([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),}
+    \idr{([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)},
 
     which follows directly from the definition of \idr{++}.
 

src/Poly.lidr

@@ -764,11 +764,11 @@ Google's map/reduce distributed programming framework.
 
 Intuitively, the behavior of the \idr{fold} operation is to insert a given
 binary operator \idr{f} between every pair of elements in a given list. For
-example, \idr{fold plus [1,2,3,4]} intuitively means \idr{1+2+3+4}. To make this
+example, \idr{fold (+) [1,2,3,4]} intuitively means \idr{1+2+3+4}. To make this
 precise, we also need a "starting element" that serves as the initial second
 input to \idr{f}. So, for example,
 
-\idr{fold plus [1,2,3,4] 0}
+\idr{fold (+) [1,2,3,4] 0}
 
 yields