get_bind — Mathlib

English

get (bind s f) equals get (f (get s)) under termination assumptions.

Русский

get (bind s f) = get (f (get s)) при предпосылках терминaции.

LaTeX

$$$$ \operatorname{get}(\operatorname{bind} s f) = \operatorname{get}(f(\operatorname{get} s)). $$$$

Lean4

@[simp]
theorem get_bind (s : Computation α) (f : α → Computation β) [Terminates s] [Terminates (f (get s))] :
    get (bind s f) = get (f (get s)) :=
  get_eq_of_mem _ (mem_bind (get_mem s) (get_mem (f (get s))))

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