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