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
    • PLift.pure = PLift.up
    Instances For
      def PLift.seq {α : Sort u} {β : Sort v} (f : PLift (αβ)) (x : UnitPLift α) :

      Applicative sequencing.

      Equations
      • f.seq x = { down := f.down (x ()).down }
      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
        • a.bind f = f a.down
        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 : β) :
          (PLift.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
            • ULift.pure = ULift.up
            Instances For
              def ULift.seq {α : Type u_1} {β : Type u_2} (f : ULift (αβ)) (x : UnitULift α) :

              Applicative sequencing.

              Equations
              • f.seq x = { down := f.down (x ()).down }
              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
                • a.bind f = f a.down
                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 : β) :
                  (ULift.rec fun (x : α) => b) = fun (x : ULift α) => b