@[extern lean_mk_array]

def Array.mkArray {α : Type u} (n : Nat) (v : α) : Array α

Equations

• mkArray n v = { data := List.replicate n v }

def Array.ofFn {α : Type u} {n : Nat} (f : Fin n → α) : Array α

ofFn f with f : Fin n → α returns the list whose ith element is f i.

ofFn f = #[f 0, f 1, ... , f(n - 1)]

Equations

• Array.ofFn f = Array.ofFn.go f 0 (Array.mkEmpty n)

@[irreducible]

def Array.ofFn.go {α : Type u} {n : Nat} (f : Fin n → α) (i : Nat) (acc : Array α) : Array α

Auxiliary for ofFn. ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]

Equations

• Array.ofFn.go f i acc = if h : i < n then Array.ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc

def Array.range (n : Nat) : Array Nat

The array #[0, 1, ..., n - 1].

Equations

• Array.range n = Nat.fold (flip Array.push) n (Array.mkEmpty n)

@[simp]

theorem Array.size_mkArray {α : Type u} (n : Nat) (v : α) : (mkArray n v).size = n

instance Array.instEmptyCollection {α : Type u} : EmptyCollection (Array α)

Equations

• Array.instEmptyCollection = { emptyCollection := #[] }

instance Array.instInhabited {α : Type u} : Inhabited (Array α)

Equations

• Array.instInhabited = { default := #[] }

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

Equations

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

def Array.singleton {α : Type u} (v : α) : Array α

Equations

• Array.singleton v = mkArray 1 v

@[extern lean_array_size]

def Array.usize {α : Type u} (a : Array α) : USize

Low-level version of size that directly queries the C array object cached size. While this is not provable, usize always returns the exact size of the array since the implementation only supports arrays of size less than USize.size.

Equations

• a.usize = a.size.toUSize

@[extern lean_array_uget]

def Array.uget {α : Type u} (a : Array α) (i : USize) (h : i.toNat < a.size) : α

Low-level version of fget which is as fast as a C array read. Fin values are represented as tag pointers in the Lean runtime. Thus, fget may be slightly slower than uget.

Equations

• a.uget i h = a[i.toNat]

instance Array.instGetElemUSizeLtNatToNatSize {α : Type u} : GetElem (Array α) USize α fun (xs : Array α) (i : USize) => i.toNat < xs.size

Equations

• Array.instGetElemUSizeLtNatToNatSize = { getElem := fun (xs : Array α) (i : USize) (h : i.toNat < xs.size) => xs.uget i h }

def Array.back {α : Type u} [Inhabited α] (a : Array α) : α

Equations

• a.back = a.get! (a.size - 1)

def Array.get? {α : Type u} (a : Array α) (i : Nat) : Option α

Equations

• a.get? i = if h : i < a.size then some a[i] else none

def Array.back? {α : Type u} (a : Array α) : Option α

Equations

• a.back? = a.get? (a.size - 1)

@[reducible, inline]

abbrev Array.getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α

Equations

• a.getLit i h₁ h₂ = let_fun this := ⋯; a[i]

@[simp]

theorem Array.size_set {α : Type u} (a : Array α) (i : Fin a.size) (v : α) : (a.set i v).size = a.size

@[simp]

theorem Array.size_push {α : Type u} (a : Array α) (v : α) : (a.push v).size = a.size + 1

@[extern lean_array_uset]

def Array.uset {α : Type u} (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α

Low-level version of fset which is as fast as a C array fset. Fin values are represented as tag pointers in the Lean runtime. Thus, fset may be slightly slower than uset.

Equations

• a.uset i v h = a.set ⟨i.toNat, h⟩ v

@[extern lean_array_fswap]

def Array.swap {α : Type u} (a : Array α) (i : Fin a.size) (j : Fin a.size) : Array α

Swaps two entries in an array.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• a.swap i j = let v₁ := a.get i; let v₂ := a.get j; let a' := a.set i v₂; a'.set (⋯ ▸ j) v₁

@[extern lean_array_swap]

def Array.swap! {α : Type u} (a : Array α) (i : Nat) (j : Nat) : Array α

Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• a.swap! i j = if h₁ : i < a.size then if h₂ : j < a.size then a.swap ⟨i, h₁⟩ ⟨j, h₂⟩ else a else a

@[inline]

def Array.swapAt {α : Type u} (a : Array α) (i : Fin a.size) (v : α) : α × Array α

Equations

• a.swapAt i v = let e := a.get i; let a := a.set i v; (e, a)

@[inline]

def Array.swapAt! {α : Type u} (a : Array α) (i : Nat) (v : α) : α × Array α

Equations

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

@[extern lean_array_pop]

def Array.pop {α : Type u} (a : Array α) : Array α

Equations

• a.pop = { data := a.data.dropLast }

def Array.shrink {α : Type u} (a : Array α) (n : Nat) : Array α

Equations

• a.shrink n = Array.shrink.loop (a.size - n) a

def Array.shrink.loop {α : Type u} : Nat → Array α → Array α

Equations

• Array.shrink.loop 0 x = x
• Array.shrink.loop n.succ x = Array.shrink.loop n x.pop

@[inline]

unsafe def Array.modifyMUnsafe {α : Type u} {m : Type u → Type u_1} [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α)

Equations

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

@[implemented_by Array.modifyMUnsafe]

def Array.modifyM {α : Type u} {m : Type u → Type u_1} [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α)

Equations

• a.modifyM i f = if h : i < a.size then let idx := ⟨i, h⟩; let v := a.get idx; do let v ← f v pure (a.set idx v) else pure a

@[inline]

def Array.modify {α : Type u} (a : Array α) (i : Nat) (f : α → α) : Array α

Equations

• a.modify i f = (a.modifyM i f).run

@[inline]

def Array.modifyOp {α : Type u} (self : Array α) (idx : Nat) (f : α → α) : Array α

Equations

• self.modifyOp idx f = self.modify idx f

@[inline]

unsafe def Array.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β

We claim this unsafe implementation is correct because an array cannot have more than usizeSz elements in our runtime.

This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies as.size < usizeSz to true.

Equations

• as.forInUnsafe b f = let sz := as.usize; Array.forInUnsafe.loop as f sz 0 b

@[specialize #[]]

unsafe def Array.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → β → m (ForInStep β)) (sz : USize) (i : USize) (b : β) : m β

Equations

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

@[implemented_by Array.forInUnsafe]

def Array.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β

Reference implementation for forIn

Equations

• as.forIn b f = Array.forIn.loop as f as.size ⋯ b

def Array.forIn.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → β → m (ForInStep β)) (i : Nat) (h : i ≤ as.size) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.
• Array.forIn.loop as f 0 x b = pure b

instance Array.instForIn {α : Type u} {m : Type u_1 → Type u_2} : ForIn m (Array α) α

Equations

• Array.instForIn = { forIn := fun {β : Type u_1} [Monad m] => Array.forIn }

@[inline]

unsafe def Array.foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m β

See comment at forInUnsafe

Equations

• Array.foldlMUnsafe f init as start stop = if start < stop then if stop ≤ as.size then Array.foldlMUnsafe.fold f as (USize.ofNat start) (USize.ofNat stop) init else pure init else pure init

@[specialize #[]]

unsafe def Array.foldlMUnsafe.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (i : USize) (stop : USize) (b : β) : m β

Equations

• Array.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let __do_lift ← f b (as.uget i ⋯) Array.foldlMUnsafe.fold f as (i + 1) stop __do_lift

@[implemented_by Array.foldlMUnsafe]

def Array.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m β

Reference implementation for foldlM

Equations

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

def Array.foldlM.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (as : Array α) (stop : Nat) (h : stop ≤ as.size) (i : Nat) (j : Nat) (b : β) : m β

Equations

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

@[inline]

unsafe def Array.foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) : m β

See comment at forInUnsafe

Equations

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

@[specialize #[]]

unsafe def Array.foldrMUnsafe.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (i : USize) (stop : USize) (b : β) : m β

Equations

• Array.foldrMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let __do_lift ← f (as.uget (i - 1) ⋯) b Array.foldrMUnsafe.fold f as (i - 1) stop __do_lift

@[implemented_by Array.foldrMUnsafe]

def Array.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) : m β

Reference implementation for foldrM

Equations

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

def Array.foldrM.fold {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (as : Array α) (stop : optParam Nat 0) (i : Nat) (h : i ≤ as.size) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.
• Array.foldrM.fold f as stop 0 x b = if (0 == stop) = true then pure b else pure b

@[inline]

unsafe def Array.mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)

See comment at forInUnsafe

Equations

• Array.mapMUnsafe f as = let sz := as.usize; unsafeCast (Array.mapMUnsafe.map f sz 0 (unsafeCast as))

@[specialize #[]]

unsafe def Array.mapMUnsafe.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (sz : USize) (i : USize) (r : Array NonScalar) : m (Array PNonScalar)

Equations

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

@[implemented_by Array.mapMUnsafe]

def Array.mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β)

Reference implementation for mapM

Equations

• Array.mapM f as = Array.mapM.map f as 0 (Array.mkEmpty as.size)

@[irreducible]

def Array.mapM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) (i : Nat) (r : Array β) : m (Array β)

Equations

• Array.mapM.map f as i r = if hlt : i < as.size then do let __do_lift ← f as[i] Array.mapM.map f as (i + 1) (r.push __do_lift) else pure r

@[inline]

def Array.mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β)

Equations

• as.mapIdxM f = Array.mapIdxM.map as f as.size 0 ⋯ (Array.mkEmpty as.size)

@[specialize #[]]

def Array.mapIdxM.map {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β)

Equations

• One or more equations did not get rendered due to their size.
• Array.mapIdxM.map as f 0 j x bs = pure bs

@[inline]

def Array.findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β)

Equations

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

@[inline]

def Array.findM? {α : Type} {m : Type → Type} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α)

Equations

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

@[inline]

def Array.findIdxM? {α : Type u} {m : Type → Type u_1} [Monad m] (as : Array α) (p : α → m Bool) : m (Option Nat)

Equations

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

@[inline]

unsafe def Array.anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m Bool

Equations

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

@[specialize #[]]

unsafe def Array.anyMUnsafe.any {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (i : USize) (stop : USize) : m Bool

Equations

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

@[implemented_by Array.anyMUnsafe]

def Array.anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m Bool

Equations

• Array.anyM p as start stop = let any := fun (stop : Nat) (h : stop ≤ as.size) => Array.anyM.loop p as stop h start; if h : stop ≤ as.size then any stop h else any as.size ⋯

@[irreducible]

def Array.anyM.loop {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (stop : Nat) (h : stop ≤ as.size) (j : Nat) : m Bool

Equations

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

@[inline]

def Array.allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m Bool

Equations

• Array.allM p as start stop = do let __do_lift ← Array.anyM (fun (v : α) => do let __do_lift ← p v pure !__do_lift) as start stop pure !__do_lift

@[inline]

def Array.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β)

Equations

• as.findSomeRevM? f = Array.findSomeRevM?.find as f as.size ⋯

@[specialize #[]]

def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) (i : Nat) : i ≤ as.size → m (Option β)

Equations

• One or more equations did not get rendered due to their size.
• Array.findSomeRevM?.find as f 0 x = pure none

@[inline]

def Array.findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α)

Equations

• as.findRevM? p = as.findSomeRevM? fun (a : α) => do let __do_lift ← p a pure (if __do_lift = true then some a else none)

@[inline]

def Array.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m PUnit

Equations

• Array.forM f as start stop = Array.foldlM (fun (x : PUnit) => f) PUnit.unit as start stop

@[inline]

def Array.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) : m PUnit

Equations

• Array.forRevM f as start stop = Array.foldrM (fun (a : α) (x : PUnit) => f a) PUnit.unit as start stop

@[inline]

def Array.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : β

Equations

• Array.foldl f init as start stop = (Array.foldlM f init as start stop).run

@[inline]

def Array.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start : optParam Nat as.size) (stop : optParam Nat 0) : β

Equations

• Array.foldr f init as start stop = (Array.foldrM f init as start stop).run

@[inline]

def Array.map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β

Equations

• Array.map f as = (Array.mapM f as).run

@[inline]

def Array.mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β

Equations

• as.mapIdx f = (as.mapIdxM f).run

def Array.zipWithIndex {α : Type u} (arr : Array α) : Array (α × Nat)

Turns #[a, b] into #[(a, 0), (b, 1)].

Equations

• arr.zipWithIndex = arr.mapIdx fun (i : Fin arr.size) (a : α) => (a, ↑i)

@[inline]

def Array.find? {α : Type} (as : Array α) (p : α → Bool) : Option α

Equations

• as.find? p = (as.findM? p).run

@[inline]

def Array.findSome? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β

Equations

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

@[inline]

def Array.findSome! {α : Type u} {β : Type v} [Inhabited β] (a : Array α) (f : α → Option β) : β

Equations

• a.findSome! f = match a.findSome? f with | some b => b | none => panicWithPosWithDecl "Init.Data.Array.Basic" "Array.findSome!" 457 14 "failed to find element"

@[inline]

def Array.findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : α → Option β) : Option β

Equations

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

@[inline]

def Array.findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α

Equations

• as.findRev? p = (as.findRevM? p).run

@[inline]

def Array.findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat

Equations

• as.findIdx? p = Array.findIdx?.loop as p 0

@[irreducible]

def Array.findIdx?.loop {α : Type u} (as : Array α) (p : α → Bool) (j : Nat) : Option Nat

Equations

• Array.findIdx?.loop as p j = if h : j < as.size then if p as[j] = true then some j else Array.findIdx?.loop as p (j + 1) else none

def Array.getIdx? {α : Type u} [BEq α] (a : Array α) (v : α) : Option Nat

Equations

• a.getIdx? v = a.findIdx? fun (a : α) => a == v

@[inline]

def Array.any {α : Type u} (as : Array α) (p : α → Bool) (start : optParam Nat 0) (stop : optParam Nat as.size) : Bool

Equations

• as.any p start stop = (Array.anyM p as start stop).run

@[inline]

def Array.all {α : Type u} (as : Array α) (p : α → Bool) (start : optParam Nat 0) (stop : optParam Nat as.size) : Bool

Equations

• as.all p start stop = (Array.allM p as start stop).run

def Array.contains {α : Type u} [BEq α] (as : Array α) (a : α) : Bool

Equations

• as.contains a = as.any fun (x : α) => x == a

def Array.elem {α : Type u} [BEq α] (a : α) (as : Array α) : Bool

Equations

• Array.elem a as = as.contains a

@[inline]

def Array.getEvenElems {α : Type u} (as : Array α) : Array α

Equations

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

@[export lean_array_to_list]

def Array.toList {α : Type u} (as : Array α) : List α

Convert a Array α into an List α. This is O(n) in the size of the array.

Equations

• as.toList = Array.foldr List.cons [] as

@[inline]

def Array.toListAppend {α : Type u} (as : Array α) (l : List α) : List α

Prepends an Array α onto the front of a list. Equivalent to as.toList ++ l.

Equations

• as.toListAppend l = Array.foldr List.cons l as

instance Array.instRepr {α : Type u} [Repr α] : Repr (Array α)

Equations

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

instance Array.instToString {α : Type u} [ToString α] : ToString (Array α)

Equations

• Array.instToString = { toString := fun (a : Array α) => "#" ++ toString a.toList }

def Array.append {α : Type u} (as : Array α) (bs : Array α) : Array α

Equations

• as.append bs = Array.foldl (fun (r : Array α) (v : α) => r.push v) as bs

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

Equations

• Array.instAppend = { append := Array.append }

def Array.appendList {α : Type u} (as : Array α) (bs : List α) : Array α

Equations

• as.appendList bs = List.foldl (fun (r : Array α) (v : α) => r.push v) as bs

instance Array.instHAppendList {α : Type u} : HAppend (Array α) (List α) (Array α)

Equations

• Array.instHAppendList = { hAppend := Array.appendList }

@[inline]

def Array.concatMapM {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β)

Equations

• Array.concatMapM f as = Array.foldlM (fun (bs : Array β) (a : α) => do let __do_lift ← f a pure (bs ++ __do_lift)) #[] as

@[inline]

def Array.concatMap {α : Type u} {β : Type u_1} (f : α → Array β) (as : Array α) : Array β

Equations

• Array.concatMap f as = Array.foldl (fun (bs : Array β) (a : α) => bs ++ f a) #[] as

def Array.flatten {α : Type u} (as : Array (Array α)) : Array α

Joins array of array into a single array.

flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯] = #[a₁, a₂, ⋯, b₁, b₂, ⋯]

Equations

• as.flatten = Array.foldl (fun (r a : Array α) => r ++ a) #[] as

def «term#[_,]» : Lean.ParserDescr

Equations

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

@[irreducible, specialize #[]]

def Array.isEqvAux {α : Type u_1} (a : Array α) (b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool

Equations

• a.isEqvAux b hsz p i = if h : i < a.size then let_fun this := ⋯; p a[i] b[i] && a.isEqvAux b hsz p (i + 1) else true

@[inline]

def Array.isEqv {α : Type u_1} (a : Array α) (b : Array α) (p : α → α → Bool) : Bool

Equations

• a.isEqv b p = if h : a.size = b.size then a.isEqvAux b h p 0 else false

instance Array.instBEq {α : Type u_1} [BEq α] : BEq (Array α)

Equations

• Array.instBEq = { beq := fun (a b : Array α) => a.isEqv b BEq.beq }

@[inline]

def Array.filter {α : Type u_1} (p : α → Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : Array α

Equations

• Array.filter p as start stop = Array.foldl (fun (r : Array α) (a : α) => if p a = true then r.push a else r) #[] as start stop

@[inline]

def Array.filterM {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m (Array α)

Equations

• Array.filterM p as start stop = Array.foldlM (fun (r : Array α) (a : α) => do let __do_lift ← p a if __do_lift = true then pure (r.push a) else pure r) #[] as start stop

@[specialize #[]]

def Array.filterMapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m (Option β)) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : m (Array β)

Equations

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

@[inline]

def Array.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) : Array β

Equations

• Array.filterMap f as start stop = (Array.filterMapM f as start stop).run

@[specialize #[]]

def Array.getMax? {α : Type u_1} (as : Array α) (lt : α → α → Bool) : Option α

Equations

• as.getMax? lt = if h : 0 < as.size then let a0 := as[0]; some (Array.foldl (fun (best a : α) => if lt best a = true then a else best) a0 as 1) else none

@[inline]

def Array.partition {α : Type u_1} (p : α → Bool) (as : Array α) : Array α × Array α

Equations

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

theorem Array.ext {α : Type u_1} (a : Array α) (b : Array α) (h₁ : a.size = b.size) (h₂ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a[i] = b[i]) : a = b

theorem Array.ext.extAux {α : Type u_1} (a : List α) (b : List α) (h₁ : a.length = b.length) (h₂ : ∀ (i : Nat) (hi₁ : i < a.length) (hi₂ : i < b.length), a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩) : a = b

theorem Array.extLit {α : Type u_1} {n : Nat} (a : Array α) (b : Array α) (hsz₁ : a.size = n) (hsz₂ : b.size = n) (h : ∀ (i : Nat) (hi : i < n), a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b

@[irreducible]

def Array.indexOfAux {α : Type u_1} [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)

Equations

• a.indexOfAux v i = if h : i < a.size then let idx := ⟨i, h⟩; if (a.get idx == v) = true then some idx else a.indexOfAux v (i + 1) else none

def Array.indexOf? {α : Type u_1} [BEq α] (a : Array α) (v : α) : Option (Fin a.size)

Equations

• a.indexOf? v = a.indexOfAux v 0

@[simp]

theorem Array.size_swap {α : Type u_1} (a : Array α) (i : Fin a.size) (j : Fin a.size) : (a.swap i j).size = a.size

@[simp]

theorem Array.size_pop {α : Type u_1} (a : Array α) : a.pop.size = a.size - 1

theorem Array.reverse.termination {i : Nat} {j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i

def Array.reverse {α : Type u_1} (as : Array α) : Array α

Equations

• as.reverse = if h : as.size ≤ 1 then as else Array.reverse.loop as 0 ⟨as.size - 1, ⋯⟩

@[irreducible]

def Array.reverse.loop {α : Type u_1} (as : Array α) (i : Nat) (j : Fin as.size) : Array α

Equations

• Array.reverse.loop as i j = if h : i < ↑j then let_fun this := ⋯; let as_1 := as.swap ⟨i, ⋯⟩ j; let_fun this := ⋯; Array.reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩ else as

@[irreducible]

def Array.popWhile {α : Type u_1} (p : α → Bool) (as : Array α) : Array α

Equations

• Array.popWhile p as = if h : as.size > 0 then if p (as.get ⟨as.size - 1, ⋯⟩) = true then Array.popWhile p as.pop else as else as

def Array.takeWhile {α : Type u_1} (p : α → Bool) (as : Array α) : Array α

Equations

• Array.takeWhile p as = Array.takeWhile.go p as 0 #[]

@[irreducible]

def Array.takeWhile.go {α : Type u_1} (p : α → Bool) (as : Array α) (i : Nat) (r : Array α) : Array α

Equations

• Array.takeWhile.go p as i r = if h : i < as.size then let a := as.get ⟨i, h⟩; if p a = true then Array.takeWhile.go p as (i + 1) (r.push a) else r else r

@[irreducible]

def Array.feraseIdx {α : Type u_1} (a : Array α) (i : Fin a.size) : Array α

Remove the element at a given index from an array without bounds checks, using a Fin index.

This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations

• a.feraseIdx i = if h : ↑i + 1 < a.size then let a' := a.swap ⟨↑i + 1, h⟩ i; let i' := ⟨↑i + 1, ⋯⟩; a'.feraseIdx i' else a.pop

theorem Array.size_feraseIdx {α : Type u_1} (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1

def Array.eraseIdx {α : Type u_1} (a : Array α) (i : Nat) : Array α

Remove the element at a given index from an array, or do nothing if the index is out of bounds.

This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations

• a.eraseIdx i = if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a

def Array.erase {α : Type u_1} [BEq α] (as : Array α) (a : α) : Array α

Equations

• as.erase a = match as.indexOf? a with | none => as | some i => as.feraseIdx i

@[inline]

def Array.insertAt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α

Insert element a at position i.

Equations

• as.insertAt i a = let j := as.size; let as_1 := as.push a; Array.insertAt.loop as i as_1 ⟨j, ⋯⟩

@[irreducible]

def Array.insertAt.loop {α : Type u_1} (as : Array α) (i : Fin (as✝.size + 1)) (as : Array α) (j : Fin as.size) : Array α

Equations

• Array.insertAt.loop as✝ i as j = if ↑i < ↑j then let j' := ⟨↑j - 1, ⋯⟩; let as_1 := as.swap j' j; Array.insertAt.loop as✝ i as_1 ⟨↑j', ⋯⟩ else as

def Array.insertAt! {α : Type u_1} (as : Array α) (i : Nat) (a : α) : Array α

Insert element a at position i. Panics if i is not i ≤ as.size.

Equations

• as.insertAt! i a = if h : i ≤ as.size then as.insertAt ⟨i, ⋯⟩ a else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.insertAt!" 787 7 "invalid index"

def Array.toListLitAux {α : Type u_1} (a : Array α) (n : Nat) (hsz : a.size = n) (i : Nat) : i ≤ a.size → List α → List α

Equations

• a.toListLitAux n hsz 0 x_3 x = x
• a.toListLitAux n hsz i.succ hi x = a.toListLitAux n hsz i ⋯ (a.getLit i hsz ⋯ :: x)

def Array.toArrayLit {α : Type u_1} (a : Array α) (n : Nat) (hsz : a.size = n) : Array α

Equations

• a.toArrayLit n hsz = List.toArray (a.toListLitAux n hsz n ⋯ [])

theorem Array.ext' {α : Type u_1} {as : Array α} {bs : Array α} (h : as.data = bs.data) : as = bs

@[simp]

theorem Array.toArrayAux_eq {α : Type u_1} (as : List α) (acc : Array α) : (as.toArrayAux acc).data = acc.data ++ as

@[simp]

theorem Array.data_toArray {α : Type u_1} (as : List α) : (List.toArray as).data = as

theorem Array.toArrayLit_eq {α : Type u_1} (as : Array α) (n : Nat) (hsz : as.size = n) : as = as.toArrayLit n hsz

theorem Array.toArrayLit_eq.getLit_eq {α : Type u_1} (n : Nat) (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = as.data[i]

theorem Array.toArrayLit_eq.go {α : Type u_1} (as : Array α) (n : Nat) (hsz : as.size = n) (i : Nat) (hi : i ≤ as.size) : as.toListLitAux n hsz i hi (List.drop i as.data) = as.data

@[irreducible]

def Array.isPrefixOfAux {α : Type u_1} [BEq α] (as : Array α) (bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool

Equations

• as.isPrefixOfAux bs hle i = if h : i < as.size then let a := as[i]; let_fun this := ⋯; let b := bs[i]; if (a == b) = true then as.isPrefixOfAux bs hle (i + 1) else false else true

def Array.isPrefixOf {α : Type u_1} [BEq α] (as : Array α) (bs : Array α) : Bool

Return true iff as is a prefix of bs. That is, bs = as ++ t for some t : List α.

Equations

• as.isPrefixOf bs = if h : as.size ≤ bs.size then as.isPrefixOfAux bs h 0 else false

def Array.allDiff {α : Type u_1} [BEq α] (as : Array α) : Bool

Equations

• as.allDiff = Array.allDiffAux as 0

@[irreducible, specialize #[]]

def Array.zipWithAux {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ

Equations

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

@[inline]

def Array.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ

Equations

• as.zipWith bs f = Array.zipWithAux f as bs 0 #[]

def Array.zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) : Array (α × β)

Equations

• as.zip bs = as.zipWith bs Prod.mk

def Array.unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : Array α × Array β

Equations

• as.unzip = Array.foldl (fun (x : Array α × Array β) (x_1 : α × β) => match x with | (as, bs) => match x_1 with | (a, b) => (as.push a, bs.push b)) (#[], #[]) as

def Array.split {α : Type u_1} (as : Array α) (p : α → Bool) : Array α × Array α

Equations

• as.split p = Array.foldl (fun (x : Array α × Array α) (a : α) => match x with | (as, bs) => if p a = true then (as.push a, bs) else (as, bs.push a)) (#[], #[]) as