StateList

inductive Mathlib.Meta.FunProp.StateList (σ : Type u) (α : 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.

• nil: {σ α : Type u} → Mathlib.Meta.FunProp.StateList σ α

  .nil is the empty list.

• cons: {σ α : Type u} → α → σ → Mathlib.Meta.FunProp.StateList σ α → Mathlib.Meta.FunProp.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.

instance Mathlib.Meta.FunProp.StateList.instAppend {α : Type u} {σ : Type u} : Append (Mathlib.Meta.FunProp.StateList σ α)

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

• Mathlib.Meta.FunProp.StateListT σ m α = (σ → m (Mathlib.Meta.FunProp.StateList σ α))

@[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) : Type u

The combined state and list monad.

Equations

• Mathlib.Meta.FunProp.StateListM σ α = Mathlib.Meta.FunProp.StateListT σ Id α

@[always_inline]

instance Mathlib.Meta.FunProp.StateListT.instMonad {σ : Type u} {m : Type u → Type v} [Monad m] : Monad (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• Mathlib.Meta.FunProp.StateListT.instMonad = Monad.mk

instance Mathlib.Meta.FunProp.StateListT.instAlternative {σ : Type u} {m : Type u → Type v} [Monad m] : Alternative (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• Mathlib.Meta.FunProp.StateListT.instAlternative = Alternative.mk (fun {α : Type u} => Mathlib.Meta.FunProp.StateListT.failure) fun {α : Type u} => Mathlib.Meta.FunProp.StateListT.orElse

@[inline]

def Mathlib.Meta.FunProp.StateListT.get {σ : Type u} {m : Type u → Type v} [Monad m] : Mathlib.Meta.FunProp.StateListT σ m σ

Return the state from StateListT σ m.

Equations

• Mathlib.Meta.FunProp.StateListT.get s = pure (Mathlib.Meta.FunProp.StateList.cons s s Mathlib.Meta.FunProp.StateList.nil)

@[inline]

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

Set the state in StateListT σ m.

Equations

• Mathlib.Meta.FunProp.StateListT.set s' x = pure (Mathlib.Meta.FunProp.StateList.cons PUnit.unit s' Mathlib.Meta.FunProp.StateList.nil)

@[inline]

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

Modify and get the state in StateListT σ m.

Equations

• Mathlib.Meta.FunProp.StateListT.modifyGet f s = let a := f s; pure (Mathlib.Meta.FunProp.StateList.cons a.fst a.snd Mathlib.Meta.FunProp.StateList.nil)

@[inline]

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

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

Equations

• Mathlib.Meta.FunProp.StateListT.lift t s = do let a ← t pure (Mathlib.Meta.FunProp.StateList.cons a s Mathlib.Meta.FunProp.StateList.nil)

instance Mathlib.Meta.FunProp.StateListT.instMonadLift {σ : Type u} {m : Type u → Type v} [Monad m] : MonadLift m (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• Mathlib.Meta.FunProp.StateListT.instMonadLift = { monadLift := fun {α : Type u} => Mathlib.Meta.FunProp.StateListT.lift }

@[always_inline]

instance Mathlib.Meta.FunProp.StateListT.instMonadFunctor {σ : Type u} {m : Type u → Type v} : MonadFunctor m (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• Mathlib.Meta.FunProp.StateListT.instMonadFunctor = { monadMap := fun {α : Type u} (f : {β : Type u} → m β → m β) (x : Mathlib.Meta.FunProp.StateListT σ m α) (s : σ) => f (x s) }

@[always_inline]

instance Mathlib.Meta.FunProp.StateListT.instMonadExceptOf {σ : Type u} {m : Type u → Type v} [Monad m] {ε : Type u_1} [MonadExceptOf ε m] : MonadExceptOf ε (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• One or more equations did not get rendered due to their size.

instance Mathlib.Meta.FunProp.instMonadStateOfStateListT {σ : Type u} {m : Type u → Type v} [Monad m] : MonadStateOf σ (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• One or more equations did not get rendered due to their size.

@[always_inline]

instance Mathlib.Meta.FunProp.StateListT.monadControl {σ : Type u} {m : Type u → Type v} [Monad m] : MonadControl m (Mathlib.Meta.FunProp.StateListT σ m)

Equations

• One or more equations did not get rendered due to their size.