Documentation

Lean.Data.PersistentArray

inductive Lean.PersistentArrayNode (α : Type u) :
Instances For
    Equations
    @[reducible, inline]
    Equations
    Instances For
      structure Lean.PersistentArray (α : Type u) :
      Instances For
        Equations
        • Lean.instInhabitedPersistentArray = { default := { root := default, tail := default, size := default, shift := default, tailOff := default } }
        @[reducible, inline]
        abbrev Lean.PArray (α : Type u) :
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • a.isEmpty = (a.size == 0)
            Instances For
              Equations
              Instances For
                @[reducible, inline]
                Equations
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For
                    @[reducible, inline]
                    Equations
                    Instances For
                      def Lean.PersistentArray.get! {α : Type u} [Inhabited α] (t : Lean.PersistentArray α) (i : Nat) :
                      α
                      Equations
                      Instances For
                        Equations
                        • Lean.PersistentArray.instGetElemNatLtSizeOfInhabited = { getElem := fun (xs : Lean.PersistentArray α) (i : Nat) (x : i < xs.size) => xs.get! i }
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[specialize #[]]
                          @[specialize #[]]
                          def Lean.PersistentArray.modify {α : Type u} [Inhabited α] (t : Lean.PersistentArray α) (i : Nat) (f : αα) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[specialize #[]]
                                  def Lean.PersistentArray.foldlM {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (t : Lean.PersistentArray α) (f : βαm β) (init : β) (start : optParam Nat 0) :
                                  m β
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[specialize #[]]
                                    def Lean.PersistentArray.foldrM {α : Type u} {m : Type v → Type w} {β : Type v} [Monad m] (t : Lean.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 : Lean.PersistentArrayNode α) (b : β) :
                                      m (ForInStep β)
                                      @[specialize #[]]
                                      def Lean.PersistentArray.forIn {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (t : Lean.PersistentArray α) (init : β) (f : αβm (ForInStep β)) :
                                      m β
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        instance Lean.PersistentArray.instForIn {α : Type u} {m : Type v → Type w} :
                                        Equations
                                        • Lean.PersistentArray.instForIn = { forIn := fun {β : Type ?u.20} [Monad m] => Lean.PersistentArray.forIn }
                                        @[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 : Lean.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 : Lean.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 : Lean.PersistentArray α) (f : αm PUnit) :
                                            Equations
                                            Instances For
                                              @[inline]
                                              def Lean.PersistentArray.foldl {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : βαβ) (init : β) (start : optParam Nat 0) :
                                              β
                                              Equations
                                              • t.foldl f init start = (t.foldlM f init start).run
                                              Instances For
                                                @[inline]
                                                def Lean.PersistentArray.foldr {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : αββ) (init : β) :
                                                β
                                                Equations
                                                • t.foldr f init = (t.foldrM f init).run
                                                Instances For
                                                  @[inline]
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    • t.toArray = t.foldl Array.push #[]
                                                    Instances For
                                                      Equations
                                                      • t₁.append t₂ = if t₁.isEmpty = true then t₂ else t₂.foldl Lean.PersistentArray.push t₁
                                                      Instances For
                                                        Equations
                                                        • Lean.PersistentArray.instAppend = { append := Lean.PersistentArray.append }
                                                        @[inline]
                                                        def Lean.PersistentArray.findSome? {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : αOption β) :
                                                        Equations
                                                        • t.findSome? f = (t.findSomeM? f).run
                                                        Instances For
                                                          @[inline]
                                                          def Lean.PersistentArray.findSomeRev? {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : αOption β) :
                                                          Equations
                                                          • t.findSomeRev? f = (t.findSomeRevM? f).run
                                                          Instances For
                                                            Equations
                                                            • t.toList = (t.foldl (fun (xs : List α) (x : α) => x :: xs) []).reverse
                                                            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 : Lean.PersistentArray α) (p : αm Bool) :
                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                def Lean.PersistentArray.allM {α : Type u} {m : TypeType w} [Monad m] (a : Lean.PersistentArray α) (p : αm Bool) :
                                                                Equations
                                                                • a.allM p = do let ba.anyM fun (v : α) => do let bp v pure !b pure !b
                                                                Instances For
                                                                  @[inline]
                                                                  def Lean.PersistentArray.any {α : Type u} (a : Lean.PersistentArray α) (p : αBool) :
                                                                  Equations
                                                                  • a.any p = (a.anyM p).run
                                                                  Instances For
                                                                    @[inline]
                                                                    def Lean.PersistentArray.all {α : Type u} (a : Lean.PersistentArray α) (p : αBool) :
                                                                    Equations
                                                                    • a.all p = !a.any fun (v : α) => !p v
                                                                    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 : Lean.PersistentArray α) :
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[inline]
                                                                        def Lean.PersistentArray.map {α : Type u} {β : Type u} (f : αβ) (t : Lean.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 α) :
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      Equations
                                                                                      Instances For
                                                                                        def Array.toPArray' {α : Type u} (xs : Array α) :
                                                                                        Equations
                                                                                        Instances For