Init.Data.Array.Basic

Array.swap! a i j = if h₁ : i < Array.size a then if h₂ : j < Array.size a then Array.swap a { val := i, isLt := h₁ } { val := j, isLt := h₂ } else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swap!" 81 7 "index out of bounds" else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swap!" 82 7 "index out of bounds"

source

@[inline]

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

α × Array α

Equations

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

source

@[inline]

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

α × Array α

Equations

Array.swapAt! a i v = if h : i < Array.size a then Array.swapAt a { val := i, isLt := h } v else let_fun this := { default := v }; panicWithPosWithDecl "Init.Data.Array.Basic" "Array.swapAt!" 95 4 ("index " ++ toString i ++ " out of bounds")

source

@[extern lean_array_pop]

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

Array α

Equations

Array.pop a = { data := List.dropLast a.data }

source

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

Array α

Equations

Array.shrink a n = (fun loop => loop (Array.size a - n) a) Array.shrink.loop

source

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

Nat → Array α → Array α

Equations

Array.shrink.loop 0 x = x
Array.shrink.loop (Nat.succ n) x = Array.shrink.loop n (Array.pop x)

source

@[inline]

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

m (Array α)

Equations

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

source

@[implementedBy Array.modifyMUnsafe]

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

m (Array α)

Equations

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); (fun loop => loop 0 b) (Array.forInUnsafe.loop as f sz)

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

Array.forInUnsafe.loop as f sz i b = if i < sz then let a := Array.uget as i (_ : USize.toNat i < Array.size as); do let a ← f a b match a with | ForInStep.done b => pure b | ForInStep.yield b => Array.forInUnsafe.loop as f sz (i + 1) b else pure b

source

@[implementedBy Array.forInUnsafe]

noncomputable 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 = (fun loop => loop (Array.size as) (_ : Array.size as ≤ Array.size as) b) (Array.forIn.loop as f)

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

Array.forIn.loop as f 0 x b = pure b
Array.forIn.loop as f (Nat.succ i_2) h_2 b = (fun h' => let_fun this := (_ : Array.size as - 1 < Array.size as); let_fun this := (_ : Array.size as - 1 - i_2 < Array.size as); do let a ← f (Array.get as { val := Array.size as - 1 - i_2, isLt := this }) b match a with | ForInStep.done b => pure b | ForInStep.yield b => Array.forIn.loop as f i_2 (_ : i_2 ≤ Array.size as) b) (_ : i_2 < Array.size as)

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

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

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

Array.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let a ← f b (Array.uget as i (_ : USize.toNat i < Array.size as)) Array.foldlMUnsafe.fold f as (i + 1) stop a

source

@[implementedBy Array.foldlMUnsafe]

noncomputable 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

Array.foldlM f init as start stop = let fold := fun stop h => (fun loop => loop (stop - start) start init) (Array.foldlM.loop f as stop h); if h : stop ≤ Array.size as then fold stop h else fold (Array.size as) (_ : Array.size as ≤ Array.size as)

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

Array.foldlM.loop f as stop h 0 j b = if hlt : j < stop then pure b else pure b
Array.foldlM.loop f as stop h (Nat.succ i') j b = if hlt : j < stop then do let a ← f b (Array.get as { val := j, isLt := (_ : j < Array.size as) }) Array.foldlM.loop f as stop h i' (j + 1) a else pure b

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

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

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

Array.foldrMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let a ← f (Array.uget as (i - 1) (_ : USize.toNat (i - 1) < Array.size as)) b Array.foldrMUnsafe.fold f as (i - 1) stop a

source

@[implementedBy Array.foldrMUnsafe]

noncomputable 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

Array.foldrM f init as start stop = (fun fold => if h : start ≤ Array.size as then if stop < start then fold start h init else pure init else if stop < Array.size as then fold (Array.size as) (_ : Array.size as ≤ Array.size as) init else pure init) (Array.foldrM.fold f as stop)

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

Array.foldrM.fold f as stop 0 x b = if (0 == stop) = true then pure b else pure b
Array.foldrM.fold f as stop (Nat.succ i_2) h_2 b = if (Nat.succ i_2 == stop) = true then pure b else let_fun this := (_ : i_2 < Array.size as); do let a ← f (Array.get as { val := i_2, isLt := this }) b Array.foldrM.fold f as stop i_2 (_ : i_2 ≤ Array.size as) a

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); (fun map => unsafeCast (map 0 (unsafeCast as))) (Array.mapMUnsafe.map f sz)

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

Array.mapMUnsafe.map f sz i r = if i < sz then let v := Array.uget r i (_ : USize.toNat i < Array.size r); let r := Array.uset r i default (_ : USize.toNat i < Array.size r); do let vNew ← f (unsafeCast v) Array.mapMUnsafe.map f sz (i + 1) (Array.uset r i (unsafeCast vNew) (_ : USize.toNat i < Array.size r)) else pure (unsafeCast r)

source

@[implementedBy Array.mapMUnsafe]

noncomputable 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 = (fun map => map (Array.size as) 0 (_ : Array.size as + 0 = Array.size as + 0) (Array.mkEmpty (Array.size as))) (Array.mapIdxM.map as f)

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

Array.mapIdxM.map as f 0 j x bs = pure bs
Array.mapIdxM.map as f (Nat.succ i_2) j inv_2 bs = (fun this => let idx := { val := j, isLt := this }; let_fun this := (_ : i_2 + (j + 1) = Array.size as); do let a ← f idx (Array.get as idx) Array.mapIdxM.map as f i_2 (j + 1) this (Array.push bs a)) (_ : j < Array.size as)

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

Array.findSomeM? as f = do let r ← forIn as { fst := none, snd := PUnit.unit } fun a r => let r := r.snd; do let a ← f a match a with | some b => pure (ForInStep.done { fst := some b, snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → m (Option β) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure (some a)

source

@[inline]

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

m (Option α)

Equations

Array.findM? as p = do let r ← forIn as { fst := none, snd := PUnit.unit } fun a r => let r := r.snd; do let a_1 ← p a if a_1 = true then pure (ForInStep.done { fst := some a, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → m (Option α) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure (some a)

source

@[inline]

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

m (Option Nat)

Equations

Array.findIdxM? as p = let i := 0; do let r ← forIn as { fst := none, snd := i } fun a r => let r := r.snd; let i := r; do let a ← p a let _do_jp : Nat → PUnit → m (ForInStep (MProd (Option (Option Nat)) Nat)) := fun i y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := i }) if a = true then pure (ForInStep.done { fst := some (some i), snd := i }) else do let y ← pure PUnit.unit _do_jp i y let x : Nat := r.snd let i : Nat := x let _do_jp : PUnit → m (Option Nat) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

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 = (fun any => if start < stop then if stop ≤ Array.size as then any (USize.ofNat start) (USize.ofNat stop) else pure false else pure false) (Array.anyMUnsafe.any p as)

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

Array.anyMUnsafe.any p as i stop = if (i == stop) = true then pure false else do let a ← p (Array.uget as i (_ : USize.toNat i < Array.size as)) if a = true then pure true else Array.anyMUnsafe.any p as (i + 1) stop

source

@[implementedBy Array.anyMUnsafe]

noncomputable 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 => (fun loop => loop (stop - start) start) (Array.anyM.loop p as stop h); 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) (i : Nat) (j : Nat) :

m Bool

Equations

Array.anyM.loop p as stop h 0 j = if hlt : j < stop then pure false else pure false
Array.anyM.loop p as stop h (Nat.succ i') j = if hlt : j < stop then do let a ← p (Array.get as { val := j, isLt := (_ : j < Array.size as) }) if a = true then pure true else Array.anyM.loop p as stop h i' (j + 1) else pure false

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 0 (Array.size as) 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 = (fun find => find (Array.size as) (_ : Array.size as ≤ Array.size as)) (Array.findSomeRevM?.find as f)

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

Array.findSomeRevM?.find as f 0 x = pure none
Array.findSomeRevM?.find as f (Nat.succ i_1) h_1 = (fun this => do let r ← f (Array.get as { val := i_1, isLt := this }) match r with | some v => pure r | none => let_fun this := (_ : i_1 ≤ Array.size as); Array.findSomeRevM?.find as f i_1 this) (_ : i_1 < Array.size as)

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

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

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 = (fun loop => loop (Array.size as) 0 (_ : Array.size as + 0 = Array.size as + 0)) (Array.findIdx?.loop as p)

source

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

Option Nat

Equations

Array.findIdx?.loop as p 0 j x = if hlt : j < Array.size as then False.elim (_ : False) else none
Array.findIdx?.loop as p (Nat.succ i_2) j inv_2 = if hlt : j < Array.size as then if p (Array.get as { val := j, isLt := hlt }) = true then some j else let_fun this := (_ : i_2 + (j + 1) = Array.size as); Array.findIdx?.loop as p i_2 (j + 1) this else none

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; (fun rev => rev as 0) (Array.reverse.rev n mid)

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

Array.getEvenElems as = (fun a => a.snd) (Array.foldl (fun x a => match x with | (even, r) => if even = true then (false, Array.push r a) else (true, r)) (true, Array.empty) as 0 (Array.size as))

source

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

Array.instReprArray = { reprPrec := fun a n => let x := { format := repr }; match x with | x_1 => if (Array.size a == 0) = true then Std.Format.text "#[]" else Std.Format.bracketFill "#[" (Lean.Format.joinSep (Array.toList a) (Std.Format.text "," ++ Lean.Format.line)) "]" }

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

«term#[_,]» = Lean.ParserDescr.node `«term#[_,]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.cat `term 0) ", " (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]"))

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

Array.isEqvAux a b hsz p i = if h : i < Array.size a then let aidx := { val := i, isLt := h }; let bidx := { val := i, isLt := (_ : i < Array.size b) }; match p (Array.get a aidx) (Array.get b bidx) with | true => Array.isEqvAux a b hsz p (i + 1) | false => false else true

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

Array.filterMapM f as start stop = Array.foldlM (fun bs a => do let a ← f a match a with | some b => pure (Array.push bs b) | none => pure bs) #[] as start stop

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

Array.getMax? as lt = if h : 0 < Array.size as then let a0 := Array.get as { val := 0, isLt := h }; some (Array.foldl (fun best a => if lt best a = true then a else best) a0 as 1 (Array.size as)) else none

source

@[inline]

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

Array α × Array α

Equations

Array.partition p as = Id.run (let bs := #[]; let cs := #[]; do let r ← forIn as { fst := bs, snd := cs } fun a r => let bs := r.fst; let cs := r.snd; if p a = true then let bs := Array.push bs a; do pure PUnit.unit pure (ForInStep.yield { fst := bs, snd := cs }) else let cs := Array.push cs a; do pure PUnit.unit pure (ForInStep.yield { fst := bs, snd := cs }) let x : MProd (Array α) (Array α) := r match x with | { fst := bs, snd := cs } => pure (bs, cs))

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 i hi₁ = List.get b i 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.eraseIdxAux {α : Type u_1} (i : Nat) (a : Array α) :

Array α

Equations

Array.eraseIdxAux i a = if h : i < Array.size a then let idx := { val := i, isLt := h }; let idx1 := { val := i - 1, isLt := (_ : i - 1 < Array.size a) }; let a' := Array.swap a idx idx1; let_fun this := (_ : Array.size a' - (i + 1) < Array.size a - i); Array.eraseIdxAux (i + 1) a' else Array.pop a

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.eraseIdxSzAux {α : Type u_1} (a : Array α) (i : Nat) (r : Array α) (heq : Array.size r = Array.size a) :

{ r // Array.size r = Array.size a - 1 }

Equations

Array.eraseIdxSzAux a i r heq = if h : i < Array.size r then let idx := { val := i, isLt := h }; let idx1 := { val := i - 1, isLt := (_ : i - 1 < Array.size r) }; Array.eraseIdxSzAux a (i + 1) (Array.swap r idx idx1) (_ : Array.size (Array.swap r idx idx1) = Array.size a) else { val := Array.pop r, property := (_ : Array.size (Array.pop r) = Array.size a - 1) }

source

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

{ r // Array.size r = Array.size a - 1 }

Equations

Array.eraseIdx' a i = Array.eraseIdxSzAux a (i.val + 1) a (_ : Array.size a = Array.size 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 α

Equations

Array.insertAt as i a = if i > Array.size as then panicWithPosWithDecl "Init.Data.Array.Basic" "Array.insertAt" 686 22 "invalid index" else let as := Array.push as a; Array.insertAtAux i as (Array.size as)

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 hi x = x
Array.toListLitAux a n hsz (Nat.succ i) hi x = Array.toListLitAux a n hsz i (_ : i ≤ Array.size a) (Array.getLit a i hsz (_ : i < n) :: x)

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

Array.isPrefixOfAux as bs hle i = if h : i < Array.size as then let a := Array.get as { val := i, isLt := h }; let b := Array.get bs { val := i, isLt := (_ : i < Array.size bs) }; if (a == b) = true then Array.isPrefixOfAux as bs hle (i + 1) else false else true

source

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

Bool

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

Array.zipWithAux f as bs i cs = if h : i < Array.size as then let a := Array.get as { val := i, isLt := h }; if h : i < Array.size bs then let b := Array.get bs { val := i, isLt := h }; Array.zipWithAux f as bs (i + 1) (Array.push cs (f a b)) else cs else cs

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

Array.unzip as = Array.foldl (fun x x_1 => match x with | (as, bs) => match x_1 with | (a, b) => (Array.push as a, Array.push bs b)) (#[], #[]) as 0 (Array.size as)

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)