@@ -103,14 +103,14 @@ patterns left of the ``|``. That is:
103 ``Parity (n + n)`` from the ``Even`` constructor definition. So
103 ``Parity (n + n)`` from the ``Even`` constructor definition. So
104 ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
104 ``(j + j)`` replaces ``k`` on the left side of ``|``, and the
105 ``Even`` constructor appears on the right side. The natural number
105 ``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
107 ``=`` sign.
107 ``=`` sign.
109- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
109- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
110 argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
110 argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
111 (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
111 (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
112− appears on the ride side of ``|``, again with the natural number
112+ appears on the right side of ``|``, again with the natural number
113− ``j`` used on the ride side of the ``=`` sign.
113+ ``j`` used on the right side of the ``=`` sign.
115Note that there is a function in the patterns (``+``) and repeated
115Note that there is a function in the patterns (``+``) and repeated
116occurrences of ``j`` - this is allowed because another argument has
116occurrences of ``j`` - this is allowed because another argument has