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)

Equations

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

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

Equations

• x.isNode = match x with | Lean.PersistentArrayNode.node cs => true | Lean.PersistentArrayNode.leaf vs => 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 : Lean.PersistentArrayNode α
• tail : Array α
• size : Nat
• shift : USize
• tailOff : Nat

instance Lean.instInhabitedPersistentArray : {a : Type u_1} → Inhabited (Lean.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} : Lean.PersistentArray α

Equations

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

def Lean.PersistentArray.isEmpty {α : Type u} (a : Lean.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 : USize) (shift : USize) : USize

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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 α

Equations

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

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

Equations

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

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 α

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 : Lean.PersistentArray α) (a : α) : Lean.PersistentArray α

Equations

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

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 α

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 : Lean.PersistentArray α) (f : β → α → m β) (init : β) (start : optParam 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 : Lean.PersistentArray α) (f : α → β → m β) (init : β) : m β

Equations

• t.foldrM f init = do let __do_lift ← Array.foldrM f init t.tail t.tail.size 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 : 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.

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

Equations

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

Equations

• t.findSomeM? f = do let __do_lift ← Lean.PersistentArray.findSomeMAux f t.root match __do_lift with | none => t.tail.findSomeM? f | 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 β)) : 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 β)

Equations

• t.findSomeRevM? f = do let __do_lift ← t.tail.findSomeRevM? f 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) : 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

Equations

• t.forM f = SeqRight.seqRight (Lean.PersistentArray.forMAux f t.root) fun (x : Unit) => Array.forM f t.tail 0

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

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

@[inline]

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

Equations

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

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

Equations

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

def Lean.PersistentArray.append {α : Type u} (t₁ : Lean.PersistentArray α) (t₂ : Lean.PersistentArray α) : Lean.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 (Lean.PersistentArray α)

Equations

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

@[inline]

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

Equations

• t.findSome? f = (t.findSomeM? f).run

@[inline]

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

Equations

• t.findSomeRev? f = (t.findSomeRevM? f).run

def Lean.PersistentArray.toList {α : Type u} (t : Lean.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) : 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

Equations

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

@[inline]

def Lean.PersistentArray.allM {α : Type u} {m : Type → Type w} [Monad m] (a : Lean.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 : Lean.PersistentArray α) (p : α → Bool) : Bool

Equations

• a.any p = (a.anyM p).run

@[inline]

def Lean.PersistentArray.all {α : Type u} (a : Lean.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 β) : 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 β)

Equations

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

@[inline]

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

Equations

• Lean.PersistentArray.map f t = (Lean.PersistentArray.mapM f t).run

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

Equations

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

def Lean.PersistentArray.Stats.toString (s : Lean.PersistentArray.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 Lean.PersistentArray.Stats

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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 0