English
Let f and g be codes representing partial functions. The evaluation of their composition (comp f g) on v equals the monadic bind of g.eval v with f.eval, i.e., apply g to v to obtain an intermediate list, then feed that list to f.
Русский
Пусть f и g — коды частичных функций. Оценка композиции (comp f g) на v равна связке монда g.eval(v) >>= f.eval, то есть сначала вычисляем g на v, затем подаем результат на вход f.
LaTeX
$$$(comp\\ f\\ g).eval(v) = g.eval(v) \\bind f.eval$$$
Lean4
@[simp]
theorem comp_eval (f g) : (comp f g).eval = fun v => g.eval v >>= f.eval := by simp [eval]