mathlib documentation

core.​init.​control.​lawful

core.​init.​control.​lawful

@[class]
structure is_lawful_applicative (f : Type uType v) [applicative f] :
Prop

Instances
@[simp]
theorem pure_id_seq {α : Type u} {f : Type uType v} [applicative f] [is_lawful_applicative f] (x : f α) :

@[simp]
theorem bind_pure {α : Type u} {m : Type uType v} [monad m] [is_lawful_monad m] (x : m α) :

theorem bind_ext_congr {α β : Type u} {m : Type uType v} [has_bind m] {x : m α} {f g : α → m β} :
(∀ (a : α), f a = g a)x >>= f = x >>= g

theorem map_ext_congr {α β : Type u} {m : Type uType v} [functor m] {x : m α} {f g : α → β} :
(∀ (a : α), f a = g a)f <$> x = g <$> x

@[simp]
theorem id.​map_eq {α β : Type} (x : id α) (f : α → β) :
f <$> x = f x

@[simp]
theorem id.​bind_eq {α β : Type} (x : id α) (f : α → id β) :
x >>= f = f x

@[simp]
theorem id.​pure_eq {α : Type} (a : α) :

@[ext]
theorem state_t.​ext {σ : Type u} {m : Type uType v} {α : Type u} {x x' : state_t σ m α} :
(∀ (st : σ), x.run st = x'.run st)x = x'

@[simp]
theorem state_t.​run_pure {σ : Type u} {m : Type uType v} {α : Type u} (st : σ) [monad m] (a : α) :

@[simp]
theorem state_t.​run_bind {σ : Type u} {m : Type uType v} {α β : Type u} (x : state_t σ m α) (st : σ) [monad m] (f : α → state_t σ m β) :
(x >>= f).run st = x.run st >>= λ (p : α × σ), (f p.fst).run p.snd

@[simp]
theorem state_t.​run_map {σ : Type u} {m : Type uType v} {α β : Type u} (x : state_t σ m α) (st : σ) [monad m] (f : α → β) [is_lawful_monad m] :
(f <$> x).run st = (λ (p : α × σ), (f p.fst, p.snd)) <$> x.run st

@[simp]
theorem state_t.​run_monad_lift {σ : Type u} {m : Type uType v} {α : Type u} (st : σ) [monad m] {n : Type uType u_1} [has_monad_lift_t n m] (x : n α) :

@[simp]
theorem state_t.​run_monad_map {σ : Type u} {m : Type uType v} {α : Type u} (x : state_t σ m α) (st : σ) [monad m] {m' : Type uType v} {n n' : Type uType u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n αn' α) :

@[simp]
theorem state_t.​run_adapt {σ : Type u} {m : Type uType v} {α : Type u} [monad m] {σ' σ'' : Type u} (st : σ) (split : σ → σ' × σ'') (join : σ' → σ'' → σ) (x : state_t σ' m α) :
(state_t.adapt split join x).run st = (λ (_a : σ' × σ''), _a.cases_on (λ (fst : σ') (snd : σ''), id_rhs (m × σ)) (x.run fst >>= λ (_p : α × σ'), (λ (_a : α × σ'), _a.cases_on (λ (fst : α) (snd_1 : σ'), id_rhs (m × σ)) (has_pure.pure (fst, join snd_1 snd)))) _p))) (split st)

@[simp]
theorem state_t.​run_get {σ : Type u} {m : Type uType v} (st : σ) [monad m] :

@[simp]
theorem state_t.​run_put {σ : Type u} {m : Type uType v} (st : σ) [monad m] (st' : σ) :

@[instance]
def state_t.​is_lawful_monad (m : Type uType v) [monad m] [is_lawful_monad m] (σ : Type u) :

Equations
  • _ = _
@[ext]
theorem except_t.​ext {α ε : Type u} {m : Type uType v} {x x' : except_t ε m α} :
x.run = x'.runx = x'

@[simp]
theorem except_t.​run_pure {α ε : Type u} {m : Type uType v} [monad m] (a : α) :

@[simp]
theorem except_t.​run_bind {α β ε : Type u} {m : Type uType v} (x : except_t ε m α) [monad m] (f : α → except_t ε m β) :

@[simp]
theorem except_t.​run_map {α β ε : Type u} {m : Type uType v} (x : except_t ε m α) [monad m] (f : α → β) [is_lawful_monad m] :

@[simp]
theorem except_t.​run_monad_lift {α ε : Type u} {m : Type uType v} [monad m] {n : Type uType u_1} [has_monad_lift_t n m] (x : n α) :

@[simp]
theorem except_t.​run_monad_map {α ε : Type u} {m : Type uType v} (x : except_t ε m α) [monad m] {m' : Type uType v} {n n' : Type uType u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n αn' α) :

@[instance]
def except_t.​is_lawful_monad (m : Type uType v) [monad m] [is_lawful_monad m] (ε : Type u) :

Equations
  • _ = _
@[ext]
theorem reader_t.​ext {ρ : Type u} {m : Type uType v} {α : Type u} {x x' : reader_t ρ m α} :
(∀ (r : ρ), x.run r = x'.run r)x = x'

@[simp]
theorem reader_t.​run_pure {ρ : Type u} {m : Type uType v} {α : Type u} (r : ρ) [monad m] (a : α) :

@[simp]
theorem reader_t.​run_bind {ρ : Type u} {m : Type uType v} {α β : Type u} (x : reader_t ρ m α) (r : ρ) [monad m] (f : α → reader_t ρ m β) :
(x >>= f).run r = x.run r >>= λ (a : α), (f a).run r

@[simp]
theorem reader_t.​run_map {ρ : Type u} {m : Type uType v} {α β : Type u} (x : reader_t ρ m α) (r : ρ) [monad m] (f : α → β) [is_lawful_monad m] :
(f <$> x).run r = f <$> x.run r

@[simp]
theorem reader_t.​run_monad_lift {ρ : Type u} {m : Type uType v} {α : Type u} (r : ρ) [monad m] {n : Type uType u_1} [has_monad_lift_t n m] (x : n α) :

@[simp]
theorem reader_t.​run_monad_map {ρ : Type u} {m : Type uType v} {α : Type u} (x : reader_t ρ m α) (r : ρ) [monad m] {m' : Type uType v} {n n' : Type uType u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n αn' α) :

@[simp]
theorem reader_t.​run_read {ρ : Type u} {m : Type uType v} (r : ρ) [monad m] :

@[instance]
def reader_t.​is_lawful_monad (ρ : Type u) (m : Type uType v) [monad m] [is_lawful_monad m] :

Equations
  • _ = _
@[ext]
theorem option_t.​ext {α : Type u} {m : Type uType v} {x x' : option_t m α} :
x.run = x'.runx = x'

@[simp]
theorem option_t.​run_pure {α : Type u} {m : Type uType v} [monad m] (a : α) :

@[simp]
theorem option_t.​run_bind {α β : Type u} {m : Type uType v} (x : option_t m α) [monad m] (f : α → option_t m β) :

@[simp]
theorem option_t.​run_map {α β : Type u} {m : Type uType v} (x : option_t m α) [monad m] (f : α → β) [is_lawful_monad m] :

@[simp]
theorem option_t.​run_monad_lift {α : Type u} {m : Type uType v} [monad m] {n : Type uType u_1} [has_monad_lift_t n m] (x : n α) :

@[simp]
theorem option_t.​run_monad_map {α : Type u} {m : Type uType v} (x : option_t m α) [monad m] {m' : Type uType v} {n n' : Type uType u_1} [monad m'] [monad_functor_t n n' m m'] (f : Π {α : Type u}, n αn' α) :

@[instance]
def option_t.​is_lawful_monad (m : Type uType v) [monad m] [is_lawful_monad m] :

Equations
  • _ = _