ret_bind — Mathlib

English

(bind (ret a) f) equals f a: pure return followed by bind equals applying f to a.

Русский

Связывание возвращения с функцией эквивалентно применению функции к значению: bind (ret a) f = f a.

LaTeX

$$$\\mathrm{bind}(\\mathrm{ret}\\; a, f) = f(a)$$$

Lean4

@[simp]
theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a :=
  by
  simp only [bind, map, ret.eq_1, map_nil]
  obtain ⟨a, s⟩ := f a
  cases s <;> simp

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