mathlib documentation

control.ulift

Monadic instances for ulift and plift #

In this file we define monad and is_lawful_monad instances on plift and ulift.

def plift.map {α : Sort u} {β : Sort v} (f : α → β) (a : plift α) :

Functorial action.

Equations
@[simp]
theorem plift.map_up {α : Sort u} {β : Sort v} (f : α → β) (a : α) :
plift.map f {down := a} = {down := f a}
@[simp]
def plift.pure {α : Sort u} :
α → plift α

Embedding of pure values.

Equations
def plift.seq {α : Sort u} {β : Sort v} (f : plift (α → β)) (x : plift α) :

Applicative sequencing.

Equations
@[simp]
theorem plift.seq_up {α : Sort u} {β : Sort v} (f : α → β) (x : α) :
{down := f}.seq {down := x} = {down := f x}
def plift.bind {α : Sort u} {β : Sort v} (a : plift α) (f : α → plift β) :

Monadic bind.

Equations
@[simp]
theorem plift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α → plift β) :
{down := a}.bind f = f a
@[instance]
Equations
@[simp]
theorem plift.rec.constant {α : Sort u} {β : Type v} (b : β) :
plift.rec (λ (_x : α), b) = λ (_x : plift α), b
def ulift.map {α : Type u} {β : Type v} (f : α → β) (a : ulift α) :

Functorial action.

Equations
@[simp]
theorem ulift.map_up {α : Type u} {β : Type v} (f : α → β) (a : α) :
ulift.map f {down := a} = {down := f a}
@[simp]
def ulift.pure {α : Type u} :
α → ulift α

Embedding of pure values.

Equations
def ulift.seq {α : Type u} {β : Type v} (f : ulift (α → β)) (x : ulift α) :

Applicative sequencing.

Equations
@[simp]
theorem ulift.seq_up {α : Type u} {β : Type v} (f : α → β) (x : α) :
{down := f}.seq {down := x} = {down := f x}
def ulift.bind {α : Type u} {β : Type v} (a : ulift α) (f : α → ulift β) :

Monadic bind.

Equations
@[simp]
theorem ulift.bind_up {α : Type u} {β : Type v} (a : α) (f : α → ulift β) :
{down := a}.bind f = f a
@[instance]
Equations
@[simp]
theorem ulift.rec.constant {α : Type u} {β : Sort v} (b : β) :
ulift.rec (λ (_x : α), b) = λ (_x : ulift α), b