Documentation

Mathlib.Control.ULift

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 α) :

Functorial action.

Equations
    Instances For
      @[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
        Instances For
          def PLift.seq {α : Sort u} {β : Sort v} (f : PLift (αβ)) (x : UnitPLift α) :

          Applicative sequencing.

          Equations
            Instances For
              @[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 β) :

              Monadic bind.

              Equations
                Instances For
                  @[simp]
                  theorem PLift.bind_up {α : Sort u} {β : Sort v} (a : α) (f : αPLift β) :
                  { down := a }.bind f = f a
                  @[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 α) :

                  Functorial action.

                  Equations
                    Instances For
                      @[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
                        Instances For
                          def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift (αβ)) (x : UnitULift α) :

                          Applicative sequencing.

                          Equations
                            Instances For
                              @[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 β) :

                              Monadic bind.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem ULift.bind_up {α : Type u} {β : Type v} (a : α) (f : αULift β) :
                                  { down := a }.bind f = f a
                                  @[simp]
                                  theorem ULift.rec.constant {α : Type u} {β : Sort v} (b : β) :
                                  (rec fun (x : α) => b) = fun (x : ULift α) => b