Documentation

Std.Do.SPred.SVal

State-indexed values #

source
@[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
Instances For
    source
    def Std.Do.SVal.StateTuple (σs : List (Type u)) :
    Type u

    A tuple capturing the whole state of an SVal.

    Instances For
      source
      @[instance_reducible]
      instance Std.Do.SVal.instInhabitedStateTupleNil :
      Inhabited (StateTuple [])
      source
      @[instance_reducible]
      instance Std.Do.SVal.instInhabitedStateTupleCons {σ : Type u_1} {σs : List (Type u_1)} [Inhabited σ] [Inhabited (StateTuple σs)] :
      Inhabited (StateTuple (σ :: σs))
      source
      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.

      Instances For
        source
        @[simp]
        theorem Std.Do.SVal.curry_nil {α : Type u_1} {f : StateTuple [] → α} :
        curry f = f PUnit.unit
        source
        @[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')
        source
        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.

        Instances For
          source
          @[simp]
          theorem Std.Do.SVal.uncurry_nil {σ : Type u} {s : σ} :
          uncurry s = fun (x : StateTuple []) => s
          source
          @[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
          source
          @[simp]
          theorem Std.Do.SVal.uncurry_curry {α : Type u} {σs : List (Type u)} {f : StateTuple σs → α} :
          (curry f).uncurry = f
          source
          @[simp]
          theorem Std.Do.SVal.curry_uncurry {α : Type u} {σs : List (Type u)} {f : SVal σs α} :
          curry f.uncurry = f
          source
          @[instance_reducible]
          instance Std.Do.SVal.instInhabited {α : Type u_1} {σs : List (Type u_1)} [Inhabited α] :
          Inhabited (SVal σs α)
          source
          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 σ.

          Instances
            source
            @[instance_reducible]
            instance Std.Do.SVal.instGetTyCons {σ : Type u_1} {σs : List (Type u_1)} :
            GetTy σ (σ :: σs)
            source
            @[instance_reducible]
            instance Std.Do.SVal.instGetTyCons_1 {σ₁ : Type u_1} {σs : List (Type u_1)} {σ₂ : Type u_1} [GetTy σ₁ σs] :
            GetTy σ₁ (σ₂ :: σs)
            source
            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.

            Instances For
              source
              @[simp]
              theorem Std.Do.SVal.getThe_here {σs : List (Type u)} (σ : Type u) (s : σ) :
              getThe σ s = curry fun (x : StateTuple σs) => s
              source
              @[simp]
              theorem Std.Do.SVal.getThe_there {σ : Type u} {σs : List (Type u)} [GetTy σ σs] (σ' : Type u) (s : σ') :
              getThe σ s = getThe σ