File tree 1 file changed +3
-3
lines changed
1 file changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -103,14 +103,14 @@ patterns left of the ``|``. That is:
103
103
``Parity (n + n) `` from the ``Even `` constructor definition. So
104
104
``(j + j) `` replaces ``k `` on the left side of ``| ``, and the
105
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
107
``= `` sign.
108
108
109
109
- Otherwise, when ``parity k `` evaluates to ``Odd ``, the original
110
110
argument ``k `` is refined to ``S (j + j) `` according to ``Parity (S
111
111
(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.
114
114
115
115
Note that there is a function in the patterns (``+ ``) and repeated
116
116
occurrences of ``j `` - this is allowed because another argument has
You can’t perform that action at this time.
0 commit comments