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) (α : Type u) :

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

Equations
  • Mathlib.Meta.FunProp.StateList.instAppend = { 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
@[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
  • x.run s = Mathlib.Meta.FunProp.StateList.toList <$> x s
@[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
  • x.run' s = Mathlib.Meta.FunProp.StateList.toList' <$> x s
@[reducible, inline]
abbrev Mathlib.Meta.FunProp.StateListM (σ : Type u) (α : Type u) :

The combined state and list monad.

Equations
@[always_inline]
Equations
  • Mathlib.Meta.FunProp.StateListT.instMonad = Monad.mk
Equations
  • Mathlib.Meta.FunProp.StateListT.instAlternative = Alternative.mk (fun {α : Type ?u.27} => Mathlib.Meta.FunProp.StateListT.failure) fun {α : Type ?u.27} => Mathlib.Meta.FunProp.StateListT.orElse
@[inline]

Return the state from StateListT σ m.

Equations
@[inline]

Set the state in StateListT σ m.

Equations
@[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
@[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
Equations
  • Mathlib.Meta.FunProp.StateListT.instMonadLift = { monadLift := fun {α : Type ?u.26} => 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.