Documentation

Mathlib.Tactic.FunProp.StateList

The combined state and list monad transformer. StateListT σ α is equivalent to StateT σ (ListT α) but more efficient.

WARNING: StateListT σ α m is only a monad if m is a commutative monad. For example,

def problem : StateListT Unit (StateM (Array Nat)) Unit := do
  Alternative.orElse (pure ()) (fun _ => pure ())
  StateListT.lift $ modify (·.push 0)
  StateListT.lift $ modify (·.push 1)

#eval ((problem.run' ()).run #[]).2

will yield either #[0,1,0,1], or #[0,0,1,1], depending on the order in which the actions in the do block are combined.

StateList

inductive Mathlib.Meta.FunProp.StateList (σ α : Type u) :

StateList is a List with a state associated to each element. This is used instead of List (α × σ) as it is more efficient.

  • nil {σ α : Type u} : StateList σ α

    .nil is the empty list.

  • cons {σ α : Type u} : ασStateList σ αStateList σ α

    If a : α, s : σ and l : List α, then .cons a s l, is the list with first element a with state s and l as the rest of the list.

Instances For
    def Mathlib.Meta.FunProp.StateListT (σ : Type u) (m : Type u → Type v) (α : Type u) :
    Type (max u v)

    The combined state and list monad transformer.

    Equations
      Instances For
        @[inline]
        def Mathlib.Meta.FunProp.StateListT.run {α σ : Type u} {m : Type u → Type v} [Functor m] (x : StateListT σ m α) (s : σ) :
        m (List (α × σ))

        Run x on a given state s, returning the list of values with corresponding states.

        Equations
          Instances For
            @[inline]
            def Mathlib.Meta.FunProp.StateListT.run' {α σ : Type u} {m : Type u → Type v} [Functor m] (x : StateListT σ m α) (s : σ) :
            m (List α)

            Run x on a given state s, returning the list of values.

            Equations
              Instances For
                @[reducible, inline]

                The combined state and list monad.

                Equations
                  Instances For
                    @[always_inline]
                    instance Mathlib.Meta.FunProp.StateListT.instMonad {σ : Type u} {m : Type u → Type v} [Monad m] :
                    Equations
                      @[inline]
                      def Mathlib.Meta.FunProp.StateListT.get {σ : Type u} {m : Type u → Type v} [Monad m] :
                      StateListT σ m σ

                      Return the state from StateListT σ m.

                      Equations
                        Instances For
                          @[inline]
                          def Mathlib.Meta.FunProp.StateListT.set {σ : Type u} {m : Type u → Type v} [Monad m] :
                          σStateListT σ m PUnit

                          Set the state in StateListT σ m.

                          Equations
                            Instances For
                              @[inline]
                              def Mathlib.Meta.FunProp.StateListT.modifyGet {α σ : Type u} {m : Type u → Type v} [Monad m] (f : σα × σ) :
                              StateListT σ m α

                              Modify and get the state in StateListT σ m.

                              Equations
                                Instances For
                                  @[inline]
                                  def Mathlib.Meta.FunProp.StateListT.lift {α σ : Type u} {m : Type u → Type v} [Monad m] (t : m α) :
                                  StateListT σ m α

                                  Lift an action from m α to StateListT σ m α.

                                  Equations
                                    Instances For
                                      Equations
                                        @[always_inline]
                                        Equations
                                          @[always_inline]
                                          instance Mathlib.Meta.FunProp.StateListT.instMonadExceptOf {σ : Type u} {m : Type u → Type v} [Monad m] {ε : Type u_1} [MonadExceptOf ε m] :
                                          Equations
                                            Equations
                                              @[always_inline]
                                              Equations