Documentation

Lean.Data.PersistentArray

inductive Lean.PersistentArrayNode (α : Type u) :
Instances For
    Equations
    @[inline, reducible]
    Equations
    Instances For
      structure Lean.PersistentArray (α : Type u) :
      Instances For
        Equations
        • Lean.instInhabitedPersistentArray = { default := { root := default, tail := default, size := default, shift := default, tailOff := default } }
        @[inline, reducible]
        abbrev Lean.PArray (α : Type u) :
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                @[inline, reducible]
                Equations
                Instances For
                  @[inline, reducible]
                  Equations
                  Instances For
                    @[inline, reducible]
                    Equations
                    Instances For
                      def Lean.PersistentArray.get! {α : Type u} [Inhabited α] (t : Lean.PersistentArray α) (i : Nat) :
                      α
                      Equations
                      Instances For
                        Equations
                        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
                                        Equations
                                        • Lean.PersistentArray.instForInPersistentArray = { forIn := fun {β} [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
                                          • One or more equations did not get rendered due to their size.
                                          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
                                              Instances For
                                                @[inline]
                                                def Lean.PersistentArray.foldr {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : αββ) (init : β) :
                                                β
                                                Equations
                                                Instances For
                                                  @[inline]
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • Lean.PersistentArray.instAppendPersistentArray = { append := Lean.PersistentArray.append }
                                                      @[inline]
                                                      def Lean.PersistentArray.findSome? {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : αOption β) :
                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Lean.PersistentArray.findSomeRev? {α : Type u} {β : Type u_1} (t : Lean.PersistentArray α) (f : αOption β) :
                                                        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 : 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
                                                            Instances For
                                                              @[inline]
                                                              def Lean.PersistentArray.any {α : Type u} (a : Lean.PersistentArray α) (p : αBool) :
                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                def Lean.PersistentArray.all {α : Type u} (a : Lean.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 : 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
                                                                          • One or more equations did not get rendered due to their size.
                                                                          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
                                                                                  def Array.toPArray' {α : Type u} (xs : Array α) :
                                                                                  Equations
                                                                                  Instances For