Documentation

Projects.Util.Monad

def sequence' {α : Type} {M : Type → Type} [hM : Monad M] (ms : List (M α)) :

Equations

sequence' ms = do let _ ← sequence ms pure ()

Instances For

def replicateM {α : Type} {M : Type → Type} [hM : Monad M] (n : ℕ) (m : M α) :

M (List α)

Equations

replicateM n m = sequence (List.replicate n m)

Instances For

def replicateM' {α : Type} {M : Type → Type} [hM : Monad M] (n : ℕ) (m : M α) :

Equations

replicateM' n m = sequence' (List.replicate n m)

Instances For

class MonadCnd {M : Type → Type} [hM : Monad M] (p : {α : Type} → M α → Prop) :

pure {α : Type} {x : α} : p (Pure.pure x)
bind {α β : Type} {m : M α} {f : α → M β} : p m → (∀ (x : α), p (f x)) → p (m >>= f)

Instances

@[simp]

theorem Id_pure {α : Type} :

pure = fun (a : α) => a

@[simp]

theorem Id_bind {α β : Type} {m : Id α} {f : α → Id β} :

m >>= f = f m

@[inline]

def gets {α : Type} {M : Type → Type} [hM : Monad M] {σ : Type} [hσ : MonadState σ M] (f : σ → α) :

M α

Equations

gets f = do let __do_lift ← get pure (f __do_lift)

Instances For

theorem run_run_snd {α β σ : Type} {m₁ : StateM σ α} {m₂ : StateM σ β} {x : σ} :

StateT.run m₂ (StateT.run m₁ x).2 = StateT.run (do (fun (x : α) => ()) <$> m₁ m₂) x

@[simp]

theorem run_gets {α : Type} {M : Type → Type} [hM : Monad M] {σ : Type} {f : σ → α} :

(gets f).run = (do let x ← get pure (f x)).run

@[simp]

theorem run_set {M : Type → Type} [hM : Monad M] {σ : Type} {s : σ} :

(set s).run = fun (x : σ) => pure ((), s)

@[simp]

theorem run_set' {M : Type → Type} [hM : Monad M] {σ : Type} {s : σ} :

(StateT.set s).run = fun (x : σ) => pure ((), s)

@[simp]

theorem sequence_nil {α : Type} {M : Type → Type} [hM : Monad M] :

sequence [] = pure []

@[simp]

theorem sequence_cons {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {m : M α} {ms : List (M α)} :

sequence (m :: ms) = do let x ← m let xs ← sequence ms pure (x :: xs)

@[simp]

theorem sequence'_nil {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] :

sequence' [] = pure ()

@[simp]

theorem sequence'_cons {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {m : M α} {ms : List (M α)} :

sequence' (m :: ms) = do let _ ← m sequence' ms

theorem MonadCnd.map {α β : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {p : {α : Type} → M α → Prop} [H : MonadCnd p] {f : α → β} {m : M α} (h₁ : p m) :

p (f <$> m)

theorem MonadCnd.sequence {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {p : {α : Type} → M α → Prop} [H : MonadCnd p] {ms : List (M α)} (h₁ : ∀ m ∈ ms, p m) :

p (_root_.sequence ms)

theorem MonadCnd.sequence' {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {p : {α : Type} → M α → Prop} [H : MonadCnd p] {ms : List (M α)} (h₁ : ∀ m ∈ ms, p m) :

p (_root_.sequence' ms)

theorem MonadCnd.replicateM {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {p : {α : Type} → M α → Prop} [H : MonadCnd p] {m : M α} {n : ℕ} (h₁ : p m) :

p (_root_.replicateM n m)

theorem MonadCnd.replicateM' {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {p : {α : Type} → M α → Prop} [H : MonadCnd p] {m : M α} {n : ℕ} (h₁ : p m) :

p (_root_.replicateM' n m)

theorem List.mapM_eq_sequence {α β : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {xs : List α} {f : α → M β} :

mapM f xs = sequence (map f xs)

theorem List.forM_eq_sequence' {α : Type} {M : Type → Type} [hM : Monad M] [hM₂ : LawfulMonad M] {xs : List α} {f : α → M Unit} :

xs.forM f = sequence' (map f xs)