|
=>
| M
= Succ M1
| M1 = Succ M2
| M2 = foldNat Succ Zero zero
-- по M1 выбираем второе уравнение
|
=> Succ (Succ (foldNat (add M M) Succ M2))
|
-- теперь для определения уравнения foldNat |
-- раскроем M2
|
=>
| M
= Succ M1
| M1 = Succ M2
| M2 = Zero
-- выбираем первое уравнение для foldNat:
|
=> Succ (Succ (add M M))
|
-- раскрываем самый верхний синоним:
|
=> Succ (Succ (foldNat M Succ M))
|
-- теперь, поскольку M уже вычислялось, в
|
-- памяти уже записан верхний конструктор,
|
-- мы знаем, что это Succ и выбираем второе |
-- уравнение:
|
=> Succ (Succ (Succ (foldNat M Succ M1)))
|
-- и M1 тоже уже вычислялось, сразу
|
-- выбираем второе уравнение
|----+
=> Succ (Succ (Succ (Succ (foldNat M Succ M2)))) |
-- M2 вычислено, идём на первое уравнение
|----+
=> Succ (Succ (Succ (Succ (Succ M))))
|
-- далее остаётся только подставить уже
|
-- вычисленные значения M
|
-- и вернуть значение.