@@ -270,7 +270,7 @@ because this gives the following error:
270 unexpected "in"
270 unexpected "in"
271 expecting dependent type signature
271 expecting dependent type signature
273−However if we put the proof into a seperate function like this:
273+However if we put the proof into a separate function like this:
275.. code-block:: idris
275.. code-block:: idris