- node {α : Type u} (cs : Array (PersistentArrayNode α)) : PersistentArrayNode α
- leaf {α : Type u} (vs : Array α) : PersistentArrayNode α
Instances For
Equations
Equations
Instances For
- root : PersistentArrayNode α
- tail : Array α
- size : Nat
- shift : USize
- tailOff : Nat
Instances For
Equations
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
partial def
Lean.PersistentArray.getAux
{α : Type u}
[Inhabited α]
:
PersistentArrayNode α → USize → USize → α
Equations
Instances For
instance
Lean.PersistentArray.instGetElemNatLtSizeOfInhabited
{α : Type u}
[Inhabited α]
:
GetElem (PersistentArray α) Nat α fun (as : PersistentArray α) (i : Nat) => i < as.size
Equations
partial def
Lean.PersistentArray.setAux
{α : Type u}
:
PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
Equations
Instances For
@[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 : α → α)
:
Equations
Instances For
partial def
Lean.PersistentArray.insertNewLeaf
{α : Type u}
:
PersistentArrayNode α → USize → USize → Array α → PersistentArrayNode α
Equations
Instances For
Equations
Instances For
partial def
Lean.PersistentArray.popLeaf
{α : Type u}
:
PersistentArrayNode α → Option (Array α) × Array (PersistentArrayNode α)
Equations
Instances For
@[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
Instances For
@[specialize #[]]
def
Lean.PersistentArray.foldrM
{α : Type u}
{m : Type v → Type w}
{β : Type v}
[Monad m]
(t : PersistentArray α)
(f : α → β → m β)
(init : β)
:
m β
Equations
Instances For
@[specialize #[]]
def
Lean.PersistentArray.forIn
{α : Type u}
{m : Type v → Type w}
[Monad m]
{β : Type v}
(t : PersistentArray α)
(init : β)
(f : α → β → m (ForInStep β))
:
m β
Equations
Instances For
instance
Lean.PersistentArray.instForIn
{α : Type u}
{m : Type v → Type w}
:
ForIn m (PersistentArray α) α
Equations
@[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
Instances For
@[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
Instances For
@[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
Instances For
@[inline]
def
Lean.PersistentArray.foldl
{α : Type u}
{β : Type u_1}
(t : PersistentArray α)
(f : β → α → β)
(init : β)
(start : Nat := 0)
:
β
Equations
Instances For
@[inline]
def
Lean.PersistentArray.foldr
{α : Type u}
{β : Type u_1}
(t : PersistentArray α)
(f : α → β → β)
(init : β)
:
β
Equations
Instances For
@[inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
@[inline]
def
Lean.PersistentArray.findSome?
{α : Type u}
{β : Type u_1}
(t : PersistentArray α)
(f : α → Option β)
:
Option β
Equations
Instances For
@[inline]
def
Lean.PersistentArray.findSomeRev?
{α : Type u}
{β : Type u_1}
(t : PersistentArray α)
(f : α → Option β)
:
Option β
Equations
Instances For
Equations
Instances For
@[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
Instances For
@[inline]
def
Lean.PersistentArray.allM
{α : Type u}
{m : Type → Type w}
[Monad m]
(a : PersistentArray α)
(p : α → m Bool)
:
m Bool
Equations
Instances For
@[inline]
Equations
Instances For
@[inline]
Equations
Instances For
@[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
Instances For
@[inline]
Equations
Instances For
partial def
Lean.PersistentArray.collectStats
{α : Type u}
:
PersistentArrayNode α → Stats → Nat → Stats
Equations
Instances For
Converts a list to a persistent array.