English
The evaluation of the fixed-point code (fix f) is given by the fixed-point operator PFun.fix applied to the map of f.eval, mapping a value to either its tail (when head is 0) or back to the tail via Sum.inr.
Русский
Оценка фиксационного кода (fix f) определяется фиксированной точкой оператора PFun.fix, применяемого к отображению f.eval, которое на входе v возвращает либо хвост, если headI = 0, либо повторное применение к tail.
LaTeX
$$$(fix\\ f).eval = PFun.fix\\ (\\\\lambda v. (f.eval(v)).map\\\\ (\\\\lambda w. \\text{if } w.headI=0 \\text{ then } Sum.inl(w.tail) \\text{ else } Sum.inr(w.tail)))$$$
Lean4
@[simp]
theorem fix_eval (f) :
(fix f).eval = PFun.fix fun v => (f.eval v).map fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail :=
by simp [eval]
