Init.Data.Array.Basic

Array.modifyM a i f = if h : i < Array.size a then let idx := { val := i, isLt := h }; let v := Array.get a idx; do let v ← f v pure (Array.set a idx v) else pure a

source

@[inline]

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

Array α

Equations

Array.modify a i f = Id.run (Array.modifyM a i f)

source

@[inline]

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

Array α

Equations

Array.modifyOp self idx f = Array.modify self idx f

source

@[inline]

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

m β

Equations

Array.forInUnsafe as b f = let sz := USize.ofNat (Array.size as); Array.forInUnsafe.loop as f sz 0 b

source

@[specialize]

unsafe def Array.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : 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.

source

@[implementedBy Array.forInUnsafe]

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

m β

Equations

Array.forIn as b f = Array.forIn.loop as f (Array.size as) (_ : Array.size as ≤ Array.size as) b

source

def Array.forIn.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : α → β → m (ForInStep β)) (i : Nat) (h : i ≤ Array.size as) (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

source

instance Array.instForInArray {α : Type u} {m : Type u_1 → Type u_2} :

ForIn m (Array α) α

Equations

Array.instForInArray = { forIn := fun {β} [Monad m] => Array.forIn }

source

@[inline]

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

m β

Equations

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

source

@[specialize]

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

m β

Equations

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

source

@[implementedBy Array.foldlMUnsafe]

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

m β

Equations

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

source

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

m β

Equations

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

source

@[inline]

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

m β

Equations

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

source

@[specialize]

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

m β

Equations

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

source

@[implementedBy Array.foldrMUnsafe]

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

m β

Equations

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

source

def Array.foldrM.fold {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → β → m β) (as : Array α) (stop : optParam Nat 0) (i : Nat) (h : i ≤ Array.size as) (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

source

@[inline]

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

m (Array β)

Equations

Array.mapMUnsafe f as = let sz := USize.ofNat (Array.size as); unsafeCast (Array.mapMUnsafe.map f sz 0 (unsafeCast as))

source

@[specialize]

unsafe def Array.mapMUnsafe.map {α : Type u} {β : Type v} {m : Type v → Type w} [inst : 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.

source

@[implementedBy Array.mapMUnsafe]

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

m (Array β)

Equations

Array.mapM f as = Array.foldlM (fun bs a => do let b ← f a pure (Array.push bs b)) (Array.mkEmpty (Array.size as)) as 0 (Array.size as)

source

@[inline]

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

m (Array β)

Equations

Array.mapIdxM as f = Array.mapIdxM.map as f (Array.size as) 0 (_ : Array.size as + 0 = Array.size as + 0) (Array.mkEmpty (Array.size as))

source

@[specialize]

def Array.mapIdxM.map {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : Fin (Array.size as) → α → m β) (i : Nat) (j : Nat) (inv : i + j = Array.size as) (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

source

@[inline]

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

m (Option β)

Equations

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

source

@[inline]

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

m (Option α)

Equations

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

source

@[inline]

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

m (Option Nat)

Equations

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

source

@[inline]

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

m Bool

Equations

Array.anyMUnsafe p as start stop = if start < stop then if stop ≤ Array.size as then Array.anyMUnsafe.any p as (USize.ofNat start) (USize.ofNat stop) else pure false else pure false

source

@[specialize]

unsafe def Array.anyMUnsafe.any {α : Type u} {m : Type → Type w} [inst : 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.

source

@[implementedBy Array.anyMUnsafe]

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

m Bool

Equations

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

source

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

m Bool

Equations

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

source

@[inline]

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

m Bool

Equations

Array.allM p as start stop = do let a ← Array.anyM (fun v => do let a ← p v pure !a) as start stop pure !a

source

@[inline]

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

m (Option β)

Equations

Array.findSomeRevM? as f = Array.findSomeRevM?.find as f (Array.size as) (_ : Array.size as ≤ Array.size as)

source

@[specialize]

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

(x : Nat) → x ≤ Array.size as → m (Option β)

Equations

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

source

@[inline]

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

m (Option α)

Equations

Array.findRevM? as p = Array.findSomeRevM? as fun a => do let a_1 ← p a pure (if a_1 = true then some a else none)

source

@[inline]

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

m PUnit

Equations

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

source

@[inline]

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

m PUnit

Equations

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

source

@[inline]

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

Equations

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

source

@[inline]

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

Equations

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

source

@[inline]

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

Array β

Equations

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

source

@[inline]

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

Array β

Equations

Array.mapIdx as f = Id.run (Array.mapIdxM as f)

source

@[inline]

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

Option α

Equations

Array.find? as p = Id.run (Array.findM? as p)

source

@[inline]

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

Option β

Equations

Array.findSome? as f = Id.run (Array.findSomeM? as f)

source

@[inline]

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

Equations

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

source

@[inline]

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

Option β

Equations

Array.findSomeRev? as f = Id.run (Array.findSomeRevM? as f)

source

@[inline]

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

Option α

Equations

Array.findRev? as p = Id.run (Array.findRevM? as p)

source

@[inline]

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

Option Nat

Equations

Array.findIdx? as p = Array.findIdx?.loop as p (Array.size as) 0 (_ : Array.size as + 0 = Array.size as + 0)

source

def Array.findIdx?.loop {α : Type u} (as : Array α) (p : α → Bool) (i : Nat) (j : Nat) (inv : i + j = Array.size as) :

Option Nat

Equations

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

source

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

Option Nat

Equations

Array.getIdx? a v = Array.findIdx? a fun a => a == v

source

@[inline]

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

Bool

Equations

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

source

@[inline]

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

Bool

Equations

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

source

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

Bool

Equations

Array.contains as a = Array.any as (fun b => a == b) 0 (Array.size as)

source

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

Bool

Equations

Array.elem a as = Array.contains as a

source

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

Array α

Equations

Array.reverse as = let n := Array.size as; let mid := n / 2; Array.reverse.rev n mid as 0

source

def Array.reverse.rev {α : Type u} (n : Nat) (mid : Nat) (as : Array α) (i : Nat) :

Array α

Equations

Array.reverse.rev n mid as i = if h : i < mid then Array.reverse.rev n mid (Array.swap! as i (n - i - 1)) (i + 1) else as

source

@[inline]

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

Array α

Equations

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

source

@[export lean_array_to_list]

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

List α

Equations

Array.toList as = Array.foldr List.cons [] as (Array.size as)

source

instance Array.instReprArray {α : Type u} [inst : Repr α] :

Repr (Array α)

Equations

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

source

instance Array.instToStringArray {α : Type u} [inst : ToString α] :

ToString (Array α)

Equations

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

source

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

Array α

Equations

Array.append as bs = Array.foldl (fun r v => Array.push r v) as bs 0 (Array.size bs)

source

instance Array.instAppendArray {α : Type u} :

Append (Array α)

Equations

Array.instAppendArray = { append := Array.append }

source

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

Array α

Equations

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

source

instance Array.instHAppendArrayList {α : Type u} :

HAppend (Array α) (List α) (Array α)

Equations

Array.instHAppendArrayList = { hAppend := Array.appendList }

source

@[inline]

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

m (Array β)

Equations

Array.concatMapM f as = Array.foldlM (fun bs a => do let a ← f a pure (bs ++ a)) Array.empty as 0 (Array.size as)

source

@[inline]

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

Array β

Equations

Array.concatMap f as = Array.foldl (fun bs a => bs ++ f a) Array.empty as 0 (Array.size as)

source

def «term#[_,]»:

Lean.ParserDescr

Equations

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

source

@[specialize]

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

Bool

Equations

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

source

@[inline]

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

Bool

Equations

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

source

instance Array.instBEqArray {α : Type u_1} [inst : BEq α] :

BEq (Array α)

Equations

Array.instBEqArray = { beq := fun a b => Array.isEqv a b BEq.beq }

source

@[inline]

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

Array α

Equations

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

source

@[inline]

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

m (Array α)

Equations

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

source

@[specialize]

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

m (Array β)

Equations

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

source

@[inline]

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

Array β

Equations

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

source

@[specialize]

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

Option α

Equations

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

source

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

source

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

a = b

source

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

a = b

source

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

a = b

source

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

Option (Fin (Array.size a))

Equations

Array.indexOfAux a v i = if h : i < Array.size a then let idx := { val := i, isLt := h }; if (Array.get a idx == v) = true then some idx else Array.indexOfAux a v (i + 1) else none

source

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

Option (Fin (Array.size a))

Equations

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

source

@[simp]

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

Array.size (Array.swap a i j) = Array.size a

source

@[simp]

theorem Array.size_pop {α : Type u_1} (a : Array α) :

Array.size (Array.pop a) = Array.size a - 1

source

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

Array α

Equations

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

source

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

Array α

Equations

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

source

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

Array α

Equations

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

source

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

Array α

Equations

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

source

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

Array α

Equations

Array.feraseIdx a i = Array.eraseIdxAux (i.val + 1) a

source

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

Array α

Equations

Array.eraseIdx a i = if i < Array.size a then Array.eraseIdxAux (i + 1) a else a

source

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

Array α

Equations

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

source

def Array.insertAtAux {α : Type u_1} (i : Nat) (as : Array α) (j : Nat) :

Array α

Equations

Array.insertAtAux i as j = if h : i < j then let as := Array.swap! as (j - 1) j; Array.insertAtAux i as (j - 1) else as

source

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

Array α

Insert element a at position i. Pre: i < as.size

Equations

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

source

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

i ≤ Array.size a → List α → List α

Equations

Array.toListLitAux a n hsz 0 x _fun_discr = _fun_discr
Array.toListLitAux a n hsz (Nat.succ i) hi _fun_discr = Array.toListLitAux a n hsz i (_ : i ≤ Array.size a) (Array.getLit a i hsz (_ : i < n) :: _fun_discr)

source

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

Array α

Equations

Array.toArrayLit a n hsz = List.toArray (Array.toListLitAux a n hsz n (_ : n ≤ Array.size a) [])

source

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

a = Array.toArrayLit a n hsz

source

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

Bool

Equations

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

source

def Array.isPrefixOf {α : Type u_1} [inst : 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

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

source

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

Bool

Equations

Array.allDiff as = Array.allDiffAux as 0

source

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

source

@[inline]

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

Array γ

Equations

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

source

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

Array (α × β)

Equations

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

source

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

Array α × Array β

Equations

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

source

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

Array α × Array α

Equations

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