State-indexed values

@[reducible, inline]

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

A value indexed by a curried tuple of states.

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

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

A tuple capturing the whole state of an SVal.

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

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

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

Curry a function taking a StateTuple into an SVal.

@[simp]

theorem Std.Do.SVal.curry_nil {α : Type} {f : StateTuple [] → α} : curry f = f ()

@[simp]

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

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

Uncurry an SVal into a function taking a StateTuple.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Do.SVal.curry_uncurry {α : Type} {σs : List Type} {f : SVal σs α} : curry #f = f

@[reducible, inline]

abbrev Std.Do.SVal.pure {α : Type} {σs : List Type} (a : α) : SVal σs α

Embed a pure value into an SVal.

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

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

• get : SVal σs σ

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

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

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

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

@[simp]

theorem Std.Do.SVal.getThe_here {σs : List Type} (σ : Type) (s : σ) : getThe σ s = pure s

@[simp]

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