Documentation

Mathlib.Tactic.FunProp.StateList

StateList

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

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

Instances For
    Equations
    • Mathlib.Meta.FunProp.StateList.instAppendStateList = { append := Mathlib.Meta.FunProp.StateList.append }
    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} {σ : Type u} {m : Type u → Type v} [Functor m] (x : Mathlib.Meta.FunProp.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} {σ : Type u} {m : Type u → Type v} [Functor m] (x : Mathlib.Meta.FunProp.StateListT σ m α) (s : σ) :
        m (List α)

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

        Equations
        Instances For
          @[reducible]

          The combined state and list monad.

          Equations
          Instances For
            @[always_inline]
            Equations
            • Mathlib.Meta.FunProp.StateListT.instMonadStateListT = Monad.mk
            Equations
            • One or more equations did not get rendered due to their size.
            @[inline]

            Return the state from StateListT σ m.

            Equations
            Instances For
              @[inline]

              Set the state in StateListT σ m.

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

                Modify and get the state in StateListT σ m.

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

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

                  Equations
                  Instances For
                    Equations
                    • Mathlib.Meta.FunProp.StateListT.instMonadLiftStateListT = { monadLift := fun {α : Type u} => Mathlib.Meta.FunProp.StateListT.lift }
                    @[always_inline]
                    Equations
                    • One or more equations did not get rendered due to their size.
                    @[always_inline]
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • One or more equations did not get rendered due to their size.
                    @[always_inline]
                    Equations
                    • One or more equations did not get rendered due to their size.