traverse_pure — Mathlib

English

Traversing with pure equals applying pure to the entire tree.

Русский

перебор по дереву через чистые значения эквивалентен применению чистой операции ко всему дереву.

LaTeX

$$$ t.traverse(\mathrm{pure}) = \mathrm{pure}(t) $$$

Lean4

theorem traverse_pure (t : Tree α) {m : Type u → Type*} [Applicative m] [LawfulApplicative m] :
    t.traverse (pure : α → m α) = pure t := by
  induction t with
  | nil => rw [traverse]
  | node v l r hl hr => rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

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