inductive Lean.PersistentArrayNode (α : Type u) : Type u

• node {α : Type u} (cs : Array (PersistentArrayNode α)) : PersistentArrayNode α
• leaf {α : Type u} (vs : Array α) : PersistentArrayNode α

@[implicit_reducible]

instance Lean.instInhabitedPersistentArrayNode {a✝ : Type u_1} : Inhabited (PersistentArrayNode a✝)

def Lean.instInhabitedPersistentArrayNode.default {a✝ : Type u_1} : PersistentArrayNode a✝

def Lean.PersistentArrayNode.isNode {α : Type u_1} : PersistentArrayNode α → Bool

@[reducible, inline]

abbrev Lean.PersistentArray.initShift : USize

@[reducible, inline]

abbrev Lean.PersistentArray.branching : USize

structure Lean.PersistentArray (α : Type u) : Type u

• root : PersistentArrayNode α
• tail : Array α
• size : Nat
• shift : USize
• tailOff : Nat

@[implicit_reducible]

instance Lean.instInhabitedPersistentArray {a✝ : Type u_1} : Inhabited (PersistentArray a✝)

def Lean.instInhabitedPersistentArray.default {a✝ : Type u_1} : PersistentArray a✝

@[reducible, inline]

abbrev Lean.PArray (α : Type u) : Type u

def Lean.PersistentArray.empty {α : Type u} : PersistentArray α

def Lean.PersistentArray.isEmpty {α : Type u} (a : PersistentArray α) : Bool

def Lean.PersistentArray.mkEmptyArray {α : Type u} : Array α

@[reducible, inline]

abbrev Lean.PersistentArray.mul2Shift (i shift : USize) : USize

@[reducible, inline]

abbrev Lean.PersistentArray.div2Shift (i shift : USize) : USize

@[reducible, inline]

abbrev Lean.PersistentArray.mod2Shift (i shift : USize) : USize

partial def Lean.PersistentArray.getAux {α : Type u} [Inhabited α] : PersistentArrayNode α → USize → USize → α

def Lean.PersistentArray.get! {α : Type u} [Inhabited α] (t : PersistentArray α) (i : Nat) : α

@[implicit_reducible]

instance Lean.PersistentArray.instGetElemNatLtSizeOfInhabited {α : Type u} [Inhabited α] : GetElem (PersistentArray α) Nat α fun (as : PersistentArray α) (i : Nat) => i < as.size

partial def Lean.PersistentArray.setAux {α : Type u} : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α

def Lean.PersistentArray.set {α : Type u} (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α

@[specialize #[]]

partial def Lean.PersistentArray.modifyAux {α : Type u} [Inhabited α] (f : α → α) : PersistentArrayNode α → USize → USize → PersistentArrayNode α

@[specialize #[]]

def Lean.PersistentArray.modify {α : Type u} [Inhabited α] (t : PersistentArray α) (i : Nat) (f : α → α) : PersistentArray α

partial def Lean.PersistentArray.mkNewPath {α : Type u} (shift : USize) (a : Array α) : PersistentArrayNode α

partial def Lean.PersistentArray.insertNewLeaf {α : Type u} : PersistentArrayNode α → USize → USize → Array α → PersistentArrayNode α

def Lean.PersistentArray.mkNewTail {α : Type u} (t : PersistentArray α) : PersistentArray α

def Lean.PersistentArray.tooBig : Nat

def Lean.PersistentArray.push {α : Type u} (t : PersistentArray α) (a : α) : PersistentArray α

partial def Lean.PersistentArray.popLeaf {α : Type u} : PersistentArrayNode α → Option (Array α) × Array (PersistentArrayNode α)

def Lean.PersistentArray.pop {α : Type u} (t : PersistentArray α) : PersistentArray α

@[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 β

@[specialize #[]]

def Lean.PersistentArray.foldrM {α : Type u} {m : Type v → Type w} {β : Type v} [Monad m] (t : PersistentArray α) (f : α → β → m β) (init : β) : m β

@[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 β

@[implicit_reducible]

instance Lean.PersistentArray.instForInOfMonad {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (PersistentArray α) α

@[specialize #[]]

partial def Lean.PersistentArray.findSomeMAux {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (f : α → m (Option β)) : PersistentArrayNode α → 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 β)

@[specialize #[]]

partial def Lean.PersistentArray.findSomeRevMAux {α : Type u} {m : Type v → Type w} [Monad m] {β : Type v} (f : α → m (Option β)) : PersistentArrayNode α → 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 β)

@[specialize #[]]

partial def Lean.PersistentArray.forMAux {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) : PersistentArrayNode α → m PUnit

@[specialize #[]]

def Lean.PersistentArray.forMFrom0 {α : Type u} {m : Type v → Type w} [Monad m] (t : PersistentArray α) (f : α → m PUnit) : m PUnit

@[specialize #[]]

def Lean.PersistentArray.forM {α : Type u} {m : Type v → Type w} [Monad m] (t : PersistentArray α) (f : α → m PUnit) (start : Nat := 0) : m PUnit

@[inline]

def Lean.PersistentArray.foldl {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : β → α → β) (init : β) (start : Nat := 0) : β

@[inline]

def Lean.PersistentArray.foldr {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : α → β → β) (init : β) : β

@[inline]

def Lean.PersistentArray.filter {α : Type u} (as : PersistentArray α) (p : α → Bool) : PersistentArray α

def Lean.PersistentArray.toArray {α : Type u} (t : PersistentArray α) : Array α

def Lean.PersistentArray.append {α : Type u} (t₁ t₂ : PersistentArray α) : PersistentArray α

@[implicit_reducible]

instance Lean.PersistentArray.instAppend {α : Type u} : Append (PersistentArray α)

@[inline]

def Lean.PersistentArray.findSome? {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : α → Option β) : Option β

@[inline]

def Lean.PersistentArray.findSomeRev? {α : Type u} {β : Type u_1} (t : PersistentArray α) (f : α → Option β) : Option β

def Lean.PersistentArray.toList {α : Type u} (t : PersistentArray α) : List α

@[specialize #[]]

partial def Lean.PersistentArray.anyMAux {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) : PersistentArrayNode α → m Bool

@[specialize #[]]

def Lean.PersistentArray.anyM {α : Type u} {m : Type → Type w} [Monad m] (t : PersistentArray α) (p : α → m Bool) : m Bool

@[inline]

def Lean.PersistentArray.allM {α : Type u} {m : Type → Type w} [Monad m] (a : PersistentArray α) (p : α → m Bool) : m Bool

@[inline]

def Lean.PersistentArray.any {α : Type u} (a : PersistentArray α) (p : α → Bool) : Bool

@[inline]

def Lean.PersistentArray.all {α : Type u} (a : PersistentArray α) (p : α → Bool) : Bool

@[specialize #[]]

partial def Lean.PersistentArray.mapMAux {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : α → m β) : PersistentArrayNode α → m (PersistentArrayNode β)

@[specialize #[]]

def Lean.PersistentArray.mapM {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : α → m β) (t : PersistentArray α) : m (PersistentArray β)

@[inline]

def Lean.PersistentArray.map {α β : Type u} (f : α → β) (t : PersistentArray α) : PersistentArray β

structure Lean.PersistentArray.Stats : Type

• numNodes : Nat
• depth : Nat
• tailSize : Nat

partial def Lean.PersistentArray.collectStats {α : Type u} : PersistentArrayNode α → Stats → Nat → Stats

def Lean.PersistentArray.stats {α : Type u} (r : PersistentArray α) : Stats

def Lean.PersistentArray.Stats.toString (s : Stats) : String

@[implicit_reducible]

instance Lean.PersistentArray.instToStringStats : ToString Stats

def Lean.mkPersistentArray {α : Type u} (n : Nat) (v : α) : PArray α

@[inline]

def Lean.mkPArray {α : Type u} (n : Nat) (v : α) : PArray α

def List.toPArray' {α : Type u} (xs : List α) : Lean.PersistentArray α

Converts a list to a persistent array.

def Array.toPArray' {α : Type u} (xs : Array α) : Lean.PersistentArray α