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.

Equations

• PLift.map f a = { down := f a.down }

@[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.

Equations

• PLift.pure = PLift.up

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

Applicative sequencing.

Equations

• f.seq x = { down := f.down (x ()).down }

@[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.

Equations

• a.bind f = f a.down

@[simp]

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

instance PLift.instMonad_mathlib : Monad PLift

Equations

• PLift.instMonad_mathlib = Monad.mk

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 : β) : (PLift.rec fun (x : α) => b) = fun (x : PLift α) => b

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

Functorial action.

Equations

• ULift.map f a = { down := f a.down }

@[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 α

Embedding of pure values.

Equations

• ULift.pure = ULift.up

def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift (α → β)) (x : Unit → ULift α) : ULift β

Applicative sequencing.

Equations

• f.seq x = { down := f.down (x ()).down }

@[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 α) (f : α → ULift β) : ULift β

Monadic bind.

Equations

• a.bind f = f a.down

@[simp]

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

instance ULift.instMonad_mathlib : Monad ULift

Equations

• ULift.instMonad_mathlib = Monad.mk

instance ULift.instLawfulFunctor_mathlib : LawfulFunctor ULift

instance ULift.instLawfulApplicative_mathlib : LawfulApplicative ULift

instance ULift.instLawfulMonad_mathlib : LawfulMonad ULift

@[simp]

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