Documentation

Init.System.ST

def EST (ε : Type) (σ : Type) :
Equations
Instances For
    @[reducible, inline]
    abbrev ST (σ : Type) :
    Equations
    Instances For
      instance instMonadEST (ε : Type) (σ : Type) :
      Monad (EST ε σ)
      Equations
      instance instMonadExceptOfEST (ε : Type) (σ : Type) :
      MonadExceptOf ε (EST ε σ)
      Equations
      instance instInhabitedEST {ε : Type} {σ : Type} {α : Type} [Inhabited ε] :
      Inhabited (EST ε σ α)
      Equations
      instance instMonadST (σ : Type) :
      Monad (ST σ)
      Equations
      class STWorld (σ : outParam Type) (m : TypeType) :
        Instances
          instance instSTWorldOfMonadLift {σ : Type} {m : TypeType} {n : TypeType} [MonadLift m n] [STWorld σ m] :
          STWorld σ n
          Equations
          • instSTWorldOfMonadLift = { }
          instance instSTWorldEST {ε : Type} {σ : Type} :
          STWorld σ (EST ε σ)
          Equations
          • instSTWorldEST = { }
          @[noinline]
          def runEST {ε : Type} {α : Type} (x : (σ : Type) → EST ε σ α) :
          Except ε α
          Equations
          Instances For
            @[noinline]
            def runST {α : Type} (x : (σ : Type) → ST σ α) :
            α
            Equations
            Instances For
              @[always_inline]
              instance instMonadLiftSTEST {ε : Type} {σ : Type} :
              MonadLift (ST σ) (EST ε σ)
              Equations
              • One or more equations did not get rendered due to their size.
              structure ST.Ref (σ : Type) (α : Type) :
              Instances For
                theorem ST.Ref.h {σ : Type} {α : Type} (self : ST.Ref σ α) :
                instance ST.instNonemptyRef {σ : Type} {α : Type} [s : Nonempty α] :
                Equations
                • =
                @[extern lean_st_mk_ref]
                opaque ST.Prim.mkRef {σ : Type} {α : Type} (a : α) :
                ST σ (ST.Ref σ α)
                @[extern lean_st_ref_get]
                opaque ST.Prim.Ref.get {σ : Type} {α : Type} (r : ST.Ref σ α) :
                ST σ α
                @[extern lean_st_ref_set]
                opaque ST.Prim.Ref.set {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
                ST σ Unit
                @[extern lean_st_ref_swap]
                opaque ST.Prim.Ref.swap {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
                ST σ α
                @[extern lean_st_ref_take]
                unsafe opaque ST.Prim.Ref.take {σ : Type} {α : Type} (r : ST.Ref σ α) :
                ST σ α
                @[extern lean_st_ref_ptr_eq]
                opaque ST.Prim.Ref.ptrEq {σ : Type} {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :
                ST σ Bool
                @[inline]
                unsafe def ST.Prim.Ref.modifyUnsafe {σ : Type} {α : Type} (r : ST.Ref σ α) (f : αα) :
                ST σ Unit
                Instances For
                  @[inline]
                  unsafe def ST.Prim.Ref.modifyGetUnsafe {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : αβ × α) :
                  ST σ β
                  Instances For
                    @[implemented_by ST.Prim.Ref.modifyUnsafe]
                    def ST.Prim.Ref.modify {σ : Type} {α : Type} (r : ST.Ref σ α) (f : αα) :
                    ST σ Unit
                    Equations
                    Instances For
                      @[implemented_by ST.Prim.Ref.modifyGetUnsafe]
                      def ST.Prim.Ref.modifyGet {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : αβ × α) :
                      ST σ β
                      Equations
                      Instances For
                        @[inline]
                        def ST.mkRef {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (a : α) :
                        m (ST.Ref σ α)
                        Equations
                        Instances For
                          @[inline]
                          def ST.Ref.get {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
                          m α
                          Equations
                          Instances For
                            @[inline]
                            def ST.Ref.set {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :
                            Equations
                            Instances For
                              @[inline]
                              def ST.Ref.swap {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :
                              m α
                              Equations
                              Instances For
                                @[inline]
                                unsafe def ST.Ref.take {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
                                m α
                                Instances For
                                  @[inline]
                                  def ST.Ref.ptrEq {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :
                                  Equations
                                  Instances For
                                    @[inline]
                                    def ST.Ref.modify {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (f : αα) :
                                    Equations
                                    Instances For
                                      @[inline]
                                      def ST.Ref.modifyGet {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} {β : Type} (r : ST.Ref σ α) (f : αβ × α) :
                                      m β
                                      Equations
                                      Instances For
                                        def ST.Ref.toMonadStateOf {σ : Type} {m : TypeType} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
                                        Equations
                                        • r.toMonadStateOf = { get := r.get, set := r.set, modifyGet := fun {α_1 : Type} => r.modifyGet }
                                        Instances For