comp_eval — Mathlib

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]

Похожие утверждения