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

• Lean.PersistentArrayNode.isNode x = match x with | Lean.PersistentArrayNode.node cs => true | Lean.PersistentArrayNode.leaf vs => false

@[inline, reducible]

abbrev Lean.PersistentArray.initShift : USize

Equations

• Lean.PersistentArray.initShift = 5

@[inline, reducible]

abbrev Lean.PersistentArray.branching : USize

Equations

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

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 } }

@[inline, reducible]

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

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

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

Equations

• Lean.PersistentArray.mkEmptyArray = Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

• Lean.PersistentArray.mod2Shift i shift = USize.land i (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

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

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

Equations

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

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

• Lean.PersistentArray.foldrM t f init = do let __do_lift ← Array.foldrM f init t.tail (Array.size 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 : 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.instForInPersistentArray {α : Type u} {m : Type v → Type w} : ForIn m (Lean.PersistentArray α) α

Equations

• Lean.PersistentArray.instForInPersistentArray = { 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

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

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

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

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

• Lean.PersistentArray.forM t 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

• Lean.PersistentArray.foldl t f init start = Id.run (Lean.PersistentArray.foldlM t f init start)

@[inline]

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

Equations

• Lean.PersistentArray.foldr t f init = Id.run (Lean.PersistentArray.foldrM t f init)

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

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

• Lean.PersistentArray.findSome? t f = Id.run (Lean.PersistentArray.findSomeM? t f)

@[inline]

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

Equations

• Lean.PersistentArray.findSomeRev? t f = Id.run (Lean.PersistentArray.findSomeRevM? t f)

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

Equations

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

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

• Lean.PersistentArray.anyM t 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

• Lean.PersistentArray.allM a p = do let b ← Lean.PersistentArray.anyM a 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

• Lean.PersistentArray.any a p = Id.run (Lean.PersistentArray.anyM a p)

@[inline]

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

Equations

• Lean.PersistentArray.all a p = !Lean.PersistentArray.any a 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 = Id.run (Lean.PersistentArray.mapM f t)

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

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

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

Equations

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

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

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

Equations

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