Content deleted Content added
Jbolden1517 (talk | contribs) →I don't get it: solving for f |
Jbolden1517 (talk | contribs) →I don't get it: Fix -> fix |
||
Line 58:
plus' g x y = g (suc x) (dec y)
: and if we had a working plus obviously ''plus' x y plus = plus x y''. But we don't. On the other hand we can keep feeding plus' more copies of plus' and actually get a plus:
plus x y =
: and then you can define your f as
f' x = (fix plus') x 1
| |||