length_bind — Mathlib

English

If termination holds, length of bind equals the sum of lengths.

Русский

При соблюдении терминaции длина бинда равна сумме длин.

LaTeX

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

Lean4

@[simp]
theorem length_bind (s : Computation α) (f : α → Computation β) [_T1 : Terminates s] [_T2 : Terminates (f (get s))] :
    length (bind s f) = length (f (get s)) + length s :=
  (results_of_terminates _).len_unique <| results_bind (results_of_terminates _) (results_of_terminates _)

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