Documentation

Init.Data.List.Monadic

Lemmas about List.mapM and List.forM. #

Monadic operations #

mapM #

source
def List.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) :
List α → m (List β)

Alternate (non-tail-recursive) form of mapM for proofs.

Equations
Instances For
    source
    @[simp]
    theorem List.mapM'_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → m β} :
    List.mapM' f [] = pure []
    source
    @[simp]
    theorem List.mapM'_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] {f : α → m β} :
    List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)
    source
    theorem List.mapM'_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
    List.mapM' f l = List.mapM f l
    source
    theorem List.mapM'_eq_mapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) (acc : List β) :
    List.mapM.loop f l acc = do let __do_lift ← List.mapM' f l pure (acc.reverse ++ __do_lift)
    source
    @[simp]
    theorem List.mapM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) :
    List.mapM f [] = pure []
    source
    @[simp]
    theorem List.mapM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] [LawfulMonad m] (f : α → m β) :
    List.mapM f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM f l pure (__do_lift :: __do_lift_1)
    source
    @[simp]
    theorem List.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) {l₁ : List α} {l₂ : List α} :
    List.mapM f (l₁ ++ l₂) = do let __do_lift ← List.mapM f l₁ let __do_lift_1 ← List.mapM f l₂ pure (__do_lift ++ __do_lift_1)

    forM #

    source
    @[simp]
    theorem List.forM_nil' {m : Type u_1 → Type u_2} {α : Type u_3} {f : α → m PUnit} [Monad m] :
    [].forM f = pure PUnit.unit
    source
    @[simp]
    theorem List.forM_cons' {m : Type u_1 → Type u_2} :
    ∀ {α : Type u_3} {a : α} {as : List α} {f : α → m PUnit} [inst : Monad m], (a :: as).forM f = do f a as.forM f
    source
    @[simp]
    theorem List.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] [LawfulMonad m] (l₁ : List α) (l₂ : List α) (f : α → m PUnit) :
    (l₁ ++ l₂).forM f = do l₁.forM f l₂.forM f