State-indexed values

@[reducible, inline]

abbrev Std.Do.SVal (σs : List (Type u)) (α : Type u) : Type u

A value indexed by a curried tuple of states.

Example:

example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl

def Std.Do.SVal.StateTuple (σs : List (Type u)) : Type u

A tuple capturing the whole state of an SVal.

instance Std.Do.SVal.instInhabitedStateTupleNil : Inhabited (StateTuple [])

instance Std.Do.SVal.instInhabitedStateTupleCons {σ : Type u_1} {σs : List (Type u_1)} [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ :: σs))

def Std.Do.SVal.curry {α : Type u} {σs : List (Type u)} (f : StateTuple σs → α) : SVal σs α

Curries a function taking a StateTuple into an SVal.

@[simp]

theorem Std.Do.SVal.curry_nil {α : Type u_1} {f : StateTuple [] → α} : curry f = f PUnit.unit

@[simp]

theorem Std.Do.SVal.curry_cons {α σ : Type u} {σs : List (Type u)} {f : StateTuple (σ :: σs) → α} {s : σ} : curry f s = curry fun (s' : StateTuple σs) => f (s, s')

def Std.Do.SVal.uncurry {α : Type u} {σs : List (Type u)} (f : SVal σs α) : StateTuple σs → α

Uncurries an SVal into a function taking a StateTuple.

@[simp]

theorem Std.Do.SVal.uncurry_nil {σ : Type u} {s : σ} : uncurry s = fun (x : StateTuple []) => s

@[simp]

theorem Std.Do.SVal.uncurry_cons {α σ : Type u} {σs : List (Type u)} {f : SVal (σ :: σs) α} {s : σ} {t : StateTuple σs} : f.uncurry (s, t) = (f s).uncurry t

@[simp]

theorem Std.Do.SVal.uncurry_curry {α : Type u} {σs : List (Type u)} {f : StateTuple σs → α} : (curry f).uncurry = f

@[simp]

theorem Std.Do.SVal.curry_uncurry {α : Type u} {σs : List (Type u)} {f : SVal σs α} : curry f.uncurry = f

instance Std.Do.SVal.instInhabited {α : Type u_1} {σs : List (Type u_1)} [Inhabited α] : Inhabited (SVal σs α)

class Std.Do.SVal.GetTy (σ : Type u) (σs : List (Type u)) : Type u

Auxiliary type class used by SVal.getThe to construct a projection from a list of state types to one of the component states.

• get : SVal σs σ

  A projection from the types σs of type σ.

instance Std.Do.SVal.instGetTyCons {σ : Type u_1} {σs : List (Type u_1)} : GetTy σ (σ :: σs)

instance Std.Do.SVal.instGetTyCons_1 {σ₁ : Type u_1} {σs : List (Type u_1)} {σ₂ : Type u_1} [GetTy σ₁ σs] : GetTy σ₁ (σ₂ :: σs)

def Std.Do.SVal.getThe {σs : List (Type u)} (σ : Type u) [GetTy σ σs] : SVal σs σ

Gets the top-most state of type σ from an SVal.

@[simp]

theorem Std.Do.SVal.getThe_here {σs : List (Type u)} (σ : Type u) (s : σ) : getThe σ s = curry fun (x : StateTuple σs) => s

@[simp]

theorem Std.Do.SVal.getThe_there {σ : Type u} {σs : List (Type u)} [GetTy σ σs] (σ' : Type u) (s : σ') : getThe σ s = getThe σ