Documentation

Lean.Data.PersistentArray

inductive Lean.PersistentArrayNode (α : Type u) :
Instances For
    Equations
      Instances For
        @[reducible, inline]
        Equations
          Instances For
            @[reducible, inline]
            Equations
              Instances For
                structure Lean.PersistentArray (α : Type u) :
                Instances For
                  @[reducible, inline]
                  abbrev Lean.PArray (α : Type u) :
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  @[reducible, inline]
                                  Equations
                                    Instances For
                                      @[reducible, inline]
                                      Equations
                                        Instances For
                                          @[reducible, inline]
                                          Equations
                                            Instances For
                                              partial def Lean.PersistentArray.getAux {α : Type u} [Inhabited α] :
                                              PersistentArrayNode αUSizeUSizeα
                                              def Lean.PersistentArray.get! {α : Type u} [Inhabited α] (t : PersistentArray α) (i : Nat) :
                                              α
                                              Equations
                                                Instances For
                                                  def Lean.PersistentArray.set {α : Type u} (t : PersistentArray α) (i : Nat) (a : α) :
                                                  Equations
                                                    Instances For
                                                      @[specialize #[]]
                                                      partial def Lean.PersistentArray.modifyAux {α : Type u} [Inhabited α] (f : αα) :
                                                      @[specialize #[]]
                                                      def Lean.PersistentArray.modify {α : Type u} [Inhabited α] (t : PersistentArray α) (i : Nat) (f : αα) :
                                                      Equations
                                                        Instances For
                                                          partial def Lean.PersistentArray.mkNewPath {α : Type u} (shift : USize) (a : Array α) :
                                                          Equations
                                                            Instances For
                                                              Equations
                                                                Instances For
                                                                  Equations
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          @[specialize #[]]
                                                                          def Lean.PersistentArray.foldlM {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (t : PersistentArray α) (f : βαm β) (init : β) (start : Nat := 0) :
                                                                          m β
                                                                          Equations
                                                                            Instances For
                                                                              @[specialize #[]]
                                                                              def Lean.PersistentArray.foldrM {α : Type u} {m : Type v → Type w} {β : Type v} [Monad m] (t : PersistentArray α) (f : αβm β) (init : β) :
                                                                              m β
                                                                              Equations
                                                                                Instances For
                                                                                  @[specialize #[]]
                                                                                  partial def Lean.PersistentArray.forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [inh : Inhabited β] (f : αβm (ForInStep β)) (n : PersistentArrayNode α) (b : β) :
                                                                                  m (ForInStep β)
                                                                                  @[specialize #[]]
                                                                                  def Lean.PersistentArray.forIn {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (t : PersistentArray α) (init : β) (f : αβm (ForInStep β)) :
                                                                                  m β
                                                                                  Equations
                                                                                    Instances For
                                                                                      instance Lean.PersistentArray.instForIn {α : Type u} {m : Type v → Type w} :
                                                                                      Equations
                                                                                        @[specialize #[]]
                                                                                        partial def Lean.PersistentArray.findSomeMAux {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (f : αm (Option β)) :
                                                                                        @[specialize #[]]
                                                                                        def Lean.PersistentArray.findSomeM? {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (t : PersistentArray α) (f : αm (Option β)) :
                                                                                        m (Option β)
                                                                                        Equations
                                                                                          Instances For
                                                                                            @[specialize #[]]
                                                                                            partial def Lean.PersistentArray.findSomeRevMAux {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (f : αm (Option β)) :
                                                                                            @[specialize #[]]
                                                                                            def Lean.PersistentArray.findSomeRevM? {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (t : PersistentArray α) (f : αm (Option β)) :
                                                                                            m (Option β)
                                                                                            Equations
                                                                                              Instances For
                                                                                                @[specialize #[]]
                                                                                                partial def Lean.PersistentArray.forMAux {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) :
                                                                                                @[specialize #[]]
                                                                                                def Lean.PersistentArray.forM {α : Type u} {m : Type v → Type w} [Monad m] (t : PersistentArray α) (f : αm PUnit) :
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Lean.PersistentArray.foldl {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : βαβ) (init : β) (start : Nat := 0) :
                                                                                                    β
                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        def Lean.PersistentArray.foldr {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : αββ) (init : β) :
                                                                                                        β
                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Lean.PersistentArray.filter {α : Type u} (as : PersistentArray α) (p : αBool) :
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        def Lean.PersistentArray.findSome? {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : αOption β) :
                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def Lean.PersistentArray.findSomeRev? {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : αOption β) :
                                                                                                                            Equations
                                                                                                                              Instances For
                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    @[specialize #[]]
                                                                                                                                    partial def Lean.PersistentArray.anyMAux {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) :
                                                                                                                                    @[specialize #[]]
                                                                                                                                    def Lean.PersistentArray.anyM {α : Type u} {m : TypeType w} [Monad m] (t : PersistentArray α) (p : αm Bool) :
                                                                                                                                    Equations
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        def Lean.PersistentArray.allM {α : Type u} {m : TypeType w} [Monad m] (a : PersistentArray α) (p : αm Bool) :
                                                                                                                                        Equations
                                                                                                                                          Instances For
                                                                                                                                            @[inline]
                                                                                                                                            def Lean.PersistentArray.any {α : Type u} (a : PersistentArray α) (p : αBool) :
                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def Lean.PersistentArray.all {α : Type u} (a : PersistentArray α) (p : αBool) :
                                                                                                                                                Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[specialize #[]]
                                                                                                                                                    partial def Lean.PersistentArray.mapMAux {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : αm β) :
                                                                                                                                                    @[specialize #[]]
                                                                                                                                                    def Lean.PersistentArray.mapM {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : αm β) (t : PersistentArray α) :
                                                                                                                                                    Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def Lean.PersistentArray.map {α β : Type u} (f : αβ) (t : PersistentArray α) :
                                                                                                                                                        Equations
                                                                                                                                                          Instances For
                                                                                                                                                            Instances For
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      def Lean.mkPersistentArray {α : Type u} (n : Nat) (v : α) :
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          def Lean.mkPArray {α : Type u} (n : Nat) (v : α) :
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              def List.toPArray' {α : Type u} (xs : List α) :

                                                                                                                                                                              Converts a list to a persistent array.

                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def Array.toPArray' {α : Type u} (xs : Array α) :
                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For