Monadic instances for ULift and PLift

In this file we define Monad and IsLawfulMonad instances on PLift and ULift.

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

Functorial action.

@[simp]

theorem PLift.map_up {α : Sort u} {β : Sort v} (f : α → β) (a : α) : PLift.map f { down := a } = { down := f a }

def PLift.pure {α : Sort u} : α → PLift α

Embedding of pure values.

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

Applicative sequencing.

@[simp]

theorem PLift.seq_up {α : Sort u} {β : Sort v} (f : α → β) (x : α) : ({ down := f }.seq fun (x_1 : Unit) => { down := x }) = { down := f x }

def PLift.bind {α : Sort u} {β : Sort v} (a : PLift α) (f : α → PLift β) : PLift β

Monadic bind.

@[simp]

theorem PLift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : α → PLift β) : { down := a }.bind f = f a

@[implicit_reducible]

instance PLift.instMonad_mathlib : Monad PLift

instance PLift.instLawfulFunctor_mathlib : LawfulFunctor PLift

instance PLift.instLawfulApplicative_mathlib : LawfulApplicative PLift

instance PLift.instLawfulMonad_mathlib : LawfulMonad PLift

@[simp]

theorem PLift.rec.constant {α : Sort u} {β : Type v} (b : β) : (rec fun (x : α) => b) = fun (x : PLift α) => b

def ULift.map {α : Type u} {β : Type v} (f : α → β) (a : ULift.{u', u} α) : ULift.{v', v} β

Functorial action.

@[simp]

theorem ULift.map_up {α : Type u} {β : Type v} (f : α → β) (a : α) : ULift.map f { down := a } = { down := f a }

def ULift.pure {α : Type u} : α → ULift.{u_1, u} α

Embedding of pure values.

def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift.{u_3, max u_1 u_2} (α → β)) (x : Unit → ULift.{u_4, u_1} α) : ULift.{u, u_2} β

Applicative sequencing.

@[simp]

theorem ULift.seq_up {α : Type u} {β : Type v} (f : α → β) (x : α) : ({ down := f }.seq fun (x_1 : Unit) => { down := x }) = { down := f x }

def ULift.bind {α : Type u} {β : Type v} (a : ULift.{u_1, u} α) (f : α → ULift.{u_2, v} β) : ULift.{u_2, v} β

Monadic bind.

@[simp]

theorem ULift.bind_up {α : Type u} {β : Type v} (a : α) (f : α → ULift.{u_1, v} β) : { down := a }.bind f = f a

@[implicit_reducible]

instance ULift.instMonad_mathlib : Monad ULift.{u_2, u_1}

instance ULift.instLawfulFunctor_mathlib : LawfulFunctor ULift.{u_2, u_1}

instance ULift.instLawfulApplicative_mathlib : LawfulApplicative ULift.{u_2, u_1}

instance ULift.instLawfulMonad_mathlib : LawfulMonad ULift.{u_2, u_1}

@[simp]

theorem ULift.rec.constant {α : Type u} {β : Sort v} (b : β) : (rec fun (x : α) => b) = fun (x : ULift.{u_1, u} α) => b