mmap_cons — Mathlib

English

Applying a monadic function to the head a and recursively to the tail v yields a monad containing the cons of the results.

Русский

Применение монадической функции к голове и далее к хвосту даёт монадный результат в виде конструкторного списка.

LaTeX

$$$\\mathrm{mmap}(f)(\\mathrm{cons}(a,v)) = \\mathrm{do}\\ let\\ h' \\leftarrow f\\ a\\; t' \\leftarrow \\mathrm{mmap}\\ f\\ v\\; \\mathrm{pure}(\\mathrm{cons}(h',t'))$$$

Lean4

@[simp]
theorem mmap_cons {m} [Monad m] {α β} (f : α → m β) (a) :
    ∀ {n} (v : Vector α n),
      mmap f (a ::ᵥ v) = do
        let h' ← f a
        let t' ← mmap f v
        pure (h' ::ᵥ t')
  | _, ⟨_, rfl⟩ => rfl

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