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

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

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

Equations

• Lean.instInhabitedPersistentArrayNode = { default := Lean.PersistentArrayNode.node default }

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

Equations

• (Lean.PersistentArrayNode.node cs).isNode = true
• (Lean.PersistentArrayNode.leaf vs).isNode = false

@[reducible, inline]

abbrev Lean.PersistentArray.initShift : USize

Equations

• Lean.PersistentArray.initShift = 5

@[reducible, inline]

abbrev Lean.PersistentArray.branching : USize

Equations

• Lean.PersistentArray.branching = USize.ofNat (2 ^ Lean.PersistentArray.initShift.toNat)

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

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

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

Equations

• Lean.instInhabitedPersistentArray = { default := { root := default, tail := default, size := default, shift := default, tailOff := default } }

@[reducible, inline]

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

Equations

• Lean.PArray α = Lean.PersistentArray α

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

Equations

• Lean.PersistentArray.empty = { }

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

Equations

• a.isEmpty = (a.size == 0)

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

Equations

• Lean.PersistentArray.mkEmptyArray = Array.mkEmpty Lean.PersistentArray.branching.toNat

@[reducible, inline]

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

Equations

• Lean.PersistentArray.mul2Shift i shift = i.shiftLeft shift

@[reducible, inline]

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

Equations

• Lean.PersistentArray.div2Shift i shift = i.shiftRight shift

@[reducible, inline]

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

Equations

• Lean.PersistentArray.mod2Shift i shift = i.land (USize.shiftLeft 1 shift - 1)

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

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

Equations

• t.get! i = if i ≥ t.tailOff then t.tail[i - t.tailOff]! else Lean.PersistentArray.getAux t.root (USize.ofNat i) t.shift

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

Equations

• Lean.PersistentArray.instGetElemNatLtSizeOfInhabited = { getElem := fun (xs : Lean.PersistentArray α) (i : Nat) (x : i < xs.size) => xs.get! i }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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 α

Equations

• One or more equations did not get rendered due to their size.

def Lean.PersistentArray.tooBig : Nat

Equations

• Lean.PersistentArray.tooBig = USize.size / 8

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

@[specialize #[]]

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

Equations

• t.foldrM f init = do let __do_lift ← Array.foldrM f init t.tail Lean.PersistentArray.foldrMAux✝ f t.root __do_lift

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

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.PersistentArray.instForIn = { forIn := fun {β : Type ?u.15} [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 β)) : 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 β)

Equations

• t.findSomeM? f = do let __do_lift ← Lean.PersistentArray.findSomeMAux f t.root match __do_lift with | none => Array.findSomeM? f t.tail | some b => pure (some b)

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

Equations

• t.findSomeRevM? f = do let __do_lift ← Array.findSomeRevM? f t.tail match __do_lift with | none => Lean.PersistentArray.findSomeRevMAux f t.root | some b => pure (some b)

@[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.forM {α : Type u} {m : Type v → Type w} [Monad m] (t : PersistentArray α) (f : α → m PUnit) : m PUnit

Equations

• t.forM f = Lean.PersistentArray.forMAux f t.root *> Array.forM f t.tail

@[inline]

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

Equations

• t.foldl f init start = (t.foldlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init start).run

@[inline]

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

Equations

• t.foldr f init = (t.foldrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init).run

@[inline]

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

Equations

• as.filter p = as.foldl (fun (asNew : Lean.PersistentArray α) (a : α) => if p a = true then asNew.push a else asNew) { }

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

Equations

• t.toArray = t.foldl Array.push #[]

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

Equations

• t₁.append t₂ = if t₁.isEmpty = true then t₂ else t₂.foldl Lean.PersistentArray.push t₁

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

Equations

• Lean.PersistentArray.instAppend = { append := Lean.PersistentArray.append }

@[inline]

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

Equations

• t.findSome? f = (t.findSomeM? fun (x : α) => pure (f x)).run

@[inline]

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

Equations

• t.findSomeRev? f = (t.findSomeRevM? fun (x : α) => pure (f x)).run

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

Equations

• t.toList = (t.foldl (fun (xs : List α) (x : α) => x :: xs) []).reverse

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

Equations

• t.anyM p = (Lean.PersistentArray.anyMAux p t.root <||> Array.anyM p t.tail)

@[inline]

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

Equations

• a.allM p = do let b ← a.anyM fun (v : α) => do let b ← p v pure !b pure !b

@[inline]

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

Equations

• a.any p = (a.anyM fun (x : α) => pure (p x)).run

@[inline]

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

Equations

• a.all p = !a.any fun (v : α) => !p v

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Lean.PersistentArray.map f t = (Lean.PersistentArray.mapM (fun (x : α) => pure (f x)) t).run

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

Equations

• r.stats = Lean.PersistentArray.collectStats r.root { numNodes := 0, depth := 0, tailSize := r.tail.size } 0

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

Equations

• s.toString = toString "{nodes := " ++ toString s.numNodes ++ toString ", depth := " ++ toString s.depth ++ toString ", tail size := " ++ toString s.tailSize ++ toString "}"

instance Lean.PersistentArray.instToStringStats : ToString Stats

Equations

• Lean.PersistentArray.instToStringStats = { toString := Lean.PersistentArray.Stats.toString }

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

Equations

• Lean.mkPersistentArray n v = n.fold (fun (x : Nat) (x : x < n) (p : Lean.PArray α) => Lean.PersistentArray.push p v) Lean.PersistentArray.empty

@[inline]

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

Equations

• Lean.mkPArray n v = Lean.mkPersistentArray n v

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

Converts a list to a persistent array.

Equations

• xs.toPArray' = List.toPArray'.loop xs { }

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 (x✝.push x_2)

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

Equations

• xs.toPArray' = Array.foldl (fun (p : Lean.PersistentArray α) (x : α) => p.push x) Lean.PersistentArray.empty xs