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

• node: {α : Type u} → Array (Lean.PersistentArrayNode α) → Lean.PersistentArrayNode α
• leaf: {α : Type u} → Array α → Lean.PersistentArrayNode α

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

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

@[inline, reducible]

abbrev Lean.PersistentArray.initShift : USize

@[inline, reducible]

abbrev Lean.PersistentArray.branching : USize

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

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

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

@[inline, reducible]

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

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

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

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

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

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

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

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

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

@[specialize #[]]

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

@[specialize #[]]

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

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

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

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

def Lean.PersistentArray.tooBig : Nat

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

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

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

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

@[specialize #[]]

def Lean.PersistentArray.foldrM {α : Type u} {m : Type v → Type w} {β : Type v} [Monad m] (t : Lean.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 : 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 β

instance Lean.PersistentArray.instForInPersistentArray {α : Type u} {m : Type v → Type w} : ForIn m (Lean.PersistentArray α) α

@[specialize #[]]

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

@[specialize #[]]

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

@[specialize #[]]

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

@[specialize #[]]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

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

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

@[inline]

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

@[inline]

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

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

@[specialize #[]]

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

@[specialize #[]]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[specialize #[]]

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

@[specialize #[]]

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

@[inline]

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

structure Lean.PersistentArray.Stats : Type

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

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

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

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

instance Lean.PersistentArray.instToStringStats : ToString Lean.PersistentArray.Stats

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

@[inline]

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

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

def List.toPArray'.loop {α : Type u} : List α → Lean.PersistentArray α → Lean.PersistentArray α

Equations

• List.toPArray'.loop [] x = x
• List.toPArray'.loop (x_2 :: xs) x = List.toPArray'.loop xs (Lean.PersistentArray.push x x_2)

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