Merge pull request #2054 from bmastenbrook/patch-1

Typo fixes for the theorem proving tutorial

docs/proofs/patterns.rst

@@ -184,7 +184,8 @@ Again, the ``fromInteger 0`` is merely due to ``Nat`` being an instance
 of the ``Num`` typeclass. So we know that ``k = plus k 0``, but how do
 we use this to update the goal to ``S k = S k``?
 
-To achieve this, provides a ``replace`` function as part of the prelude:
+To achieve this, Idris provides a ``replace`` function as part of the
+prelude:
 
 .. code-block:: idris
 
@@ -195,8 +196,8 @@ Given a proof that ``x = y``, and a property ``P`` which holds for
 ``x``, we can get a proof of the same property for ``y``, because we
 know ``x`` and ``y`` must be the same. In practice, this function can be
 a little tricky to use because in general the implicit argument ``P``
-can be hard to infer by unification, so provides a high level syntax
-which calculates the property and applies replace:
+can be hard to infer by unification, so Idris provides a high level
+syntax which calculates the property and applies ``replace``:
 
 .. code-block:: idris
 

docs/proofs/pluscomm.rst

@@ -132,7 +132,7 @@ equalities between values in different types:
 
     idris_not_php : 2 = "2"
 
-Obviously, in Idris the type ``2 = 2`` is uninhabited, and one might
+Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might
 wonder why it is useful to be able to propose equalities between values
 in different types. However, with dependent types, such equalities can
 arise naturally. For example, if two vectors are equal, their lengths
@@ -177,7 +177,7 @@ given above as Idris type declarations:
 Both of these properties (and many others) are proved for natural number
 addition in the Idris standard library, using ``(+)`` from the ``Num``
 type class rather than using ``plus`` directly. They have the names
-``plusCommutative`` and ``plusAssociatie`` respectively.
+``plusCommutative`` and ``plusAssociative`` respectively.
 
 In the remainder of this tutorial, we will explore several different
 ways of proving ``plus_commutes`` (or, to put it another way, writing