@@ -103,14 +103,14 @@ patterns left of the ``|``. That is:
103103 ``Parity (n + n)`` from the ``Even`` constructor definition. So
104104 ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
105105 ``Even`` constructor appears on the right side. The natural number
106− ``j`` in the refined pattern can be used on the ride side of the
106+ ``j`` in the refined pattern can be used on the right side of the
107107 ``=`` sign.
108108
109109- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
110110 argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
111111 (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
112− appears on the ride side of ``|``, again with the natural number
113− ``j`` used on the ride side of the ``=`` sign.
112+ appears on the right side of ``|``, again with the natural number
113+ ``j`` used on the right side of the ``=`` sign.
114114
115115Note that there is a function in the patterns (``+``) and repeated
116116occurrences of ``j`` - this is allowed because another argument has