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