Documentation

Init.Data.Array.Basic

@[extern lean_mk_array]
def Array.mkArray {α : Type u} (n : Nat) (v : α) :
Equations
@[simp]
theorem Array.size_mkArray {α : Type u} (n : Nat) (v : α) :
Equations
  • Array.instEmptyCollectionArray = { emptyCollection := Array.empty }
instance Array.instInhabitedArray {α : Type u} :
Equations
  • Array.instInhabitedArray = { default := Array.empty }
def Array.isEmpty {α : Type u} (a : Array α) :
Equations
def Array.singleton {α : Type u} (v : α) :
Equations
@[extern lean_array_uget]
def Array.uget {α : Type u} (a : Array α) (i : USize) (h : USize.toNat i < Array.size a) :
α
Equations
def Array.back {α : Type u} [inst : Inhabited α] (a : Array α) :
α
Equations
def Array.get? {α : Type u} (a : Array α) (i : Nat) :
Equations
def Array.back? {α : Type u} (a : Array α) :
Equations
@[inline]
abbrev Array.getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : Array.size a = n) (h₂ : i < n) :
α
Equations
@[simp]
theorem Array.size_set {α : Type u} (a : Array α) (i : Fin (Array.size a)) (v : α) :
@[simp]
theorem Array.size_push {α : Type u} (a : Array α) (v : α) :
@[extern lean_array_uset]
def Array.uset {α : Type u} (a : Array α) (i : USize) (v : α) (h : USize.toNat i < Array.size a) :
Equations
@[extern lean_array_fswap]
def Array.swap {α : Type u} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) :
Equations
@[extern lean_array_swap]
def Array.swap! {α : Type u} (a : Array α) (i : Nat) (j : Nat) :
Equations
@[inline]
def Array.swapAt {α : Type u} (a : Array α) (i : Fin (Array.size a)) (v : α) :
α × Array α
Equations
@[inline]
def Array.swapAt! {α : Type u} (a : Array α) (i : Nat) (v : α) :
α × Array α
Equations
@[extern lean_array_pop]
def Array.pop {α : Type u} (a : Array α) :
Equations
def Array.shrink {α : Type u} (a : Array α) (n : Nat) :
Equations
def Array.shrink.loop {α : Type u} :
NatArray αArray α
Equations
@[inline]
unsafe def Array.modifyMUnsafe {α : Type u} {m : Type uType u_1} [inst : Monad m] (a : Array α) (i : Nat) (f : αm α) :
m (Array α)
Equations
@[implementedBy Array.modifyMUnsafe]
noncomputable def Array.modifyM {α : Type u} {m : Type uType u_1} [inst : Monad m] (a : Array α) (i : Nat) (f : αm α) :
m (Array α)
Equations
@[inline]
def Array.modify {α : Type u} (a : Array α) (i : Nat) (f : αα) :
Equations
@[inline]
def Array.modifyOp {α : Type u} (self : Array α) (idx : Nat) (f : αα) :
Equations
@[inline]
unsafe def Array.forInUnsafe {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (b : β) (f : αβm (ForInStep β)) :
m β
Equations
@[specialize]
unsafe def Array.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (f : αβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
m β
Equations
@[implementedBy Array.forInUnsafe]
noncomputable def Array.forIn {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (b : β) (f : αβm (ForInStep β)) :
m β
Equations
def Array.forIn.loop {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (f : αβm (ForInStep β)) (i : Nat) (h : i Array.size as) (b : β) :
m β
Equations
instance Array.instForInArray {α : Type u} {m : Type u_1Type u_2} :
ForIn m (Array α) α
Equations
  • Array.instForInArray = { forIn := fun {β} [Monad m] => Array.forIn }
@[inline]
unsafe def Array.foldlMUnsafe {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : βαm β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
m β
Equations
@[specialize]
unsafe def Array.foldlMUnsafe.fold {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : βαm β) (as : Array α) (i : USize) (stop : USize) (b : β) :
m β
Equations
@[implementedBy Array.foldlMUnsafe]
noncomputable def Array.foldlM {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : βαm β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
m β
Equations
def Array.foldlM.loop {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : βαm β) (as : Array α) (stop : Nat) (h : stop Array.size as) (i : Nat) (j : Nat) (b : β) :
m β
Equations
@[inline]
unsafe def Array.foldrMUnsafe {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αβm β) (init : β) (as : Array α) (start : optParam Nat (Array.size as)) (stop : optParam Nat 0) :
m β
Equations
@[specialize]
unsafe def Array.foldrMUnsafe.fold {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αβm β) (as : Array α) (i : USize) (stop : USize) (b : β) :
m β
Equations
@[implementedBy Array.foldrMUnsafe]
noncomputable def Array.foldrM {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αβm β) (init : β) (as : Array α) (start : optParam Nat (Array.size as)) (stop : optParam Nat 0) :
m β
Equations
def Array.foldrM.fold {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αβm β) (as : Array α) (stop : optParam Nat 0) (i : Nat) (h : i Array.size as) (b : β) :
m β
Equations
@[inline]
unsafe def Array.mapMUnsafe {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αm β) (as : Array α) :
m (Array β)
Equations
@[specialize]
unsafe def Array.mapMUnsafe.map {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αm β) (sz : USize) (i : USize) (r : Array NonScalar) :
Equations
@[implementedBy Array.mapMUnsafe]
noncomputable def Array.mapM {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αm β) (as : Array α) :
m (Array β)
Equations
@[inline]
def Array.mapIdxM {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (f : Fin (Array.size as)αm β) :
m (Array β)
Equations
@[specialize]
def Array.mapIdxM.map {α : Type u} {β : Type v} {m : Type vType 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
@[inline]
def Array.findSomeM? {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (f : αm (Option β)) :
m (Option β)
Equations
@[inline]
def Array.findM? {α : Type} {m : TypeType} [inst : Monad m] (as : Array α) (p : αm Bool) :
m (Option α)
Equations
@[inline]
def Array.findIdxM? {α : Type u} {m : TypeType u_1} [inst : Monad m] (as : Array α) (p : αm Bool) :
Equations
@[inline]
unsafe def Array.anyMUnsafe {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
@[specialize]
unsafe def Array.anyMUnsafe.any {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Array α) (i : USize) (stop : USize) :
Equations
@[implementedBy Array.anyMUnsafe]
noncomputable def Array.anyM {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
def Array.anyM.loop {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Array α) (stop : Nat) (h : stop Array.size as) (j : Nat) :
Equations
@[inline]
def Array.allM {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
@[inline]
def Array.findSomeRevM? {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (f : αm (Option β)) :
m (Option β)
Equations
@[specialize]
def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (as : Array α) (f : αm (Option β)) :
(_fun_discr : Nat) → _fun_discr Array.size asm (Option β)
Equations
@[inline]
def Array.findRevM? {α : Type} {m : TypeType w} [inst : Monad m] (as : Array α) (p : αm Bool) :
m (Option α)
Equations
@[inline]
def Array.forM {α : Type u} {m : Type vType w} [inst : Monad m] (f : αm PUnit) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
@[inline]
def Array.forRevM {α : Type u} {m : Type vType w} [inst : Monad m] (f : αm PUnit) (as : Array α) (start : optParam Nat (Array.size as)) (stop : optParam Nat 0) :
Equations
@[inline]
def Array.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
β
Equations
@[inline]
def Array.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : Array α) (start : optParam Nat (Array.size as)) (stop : optParam Nat 0) :
β
Equations
@[inline]
def Array.map {α : Type u} {β : Type v} (f : αβ) (as : Array α) :
Equations
@[inline]
def Array.mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin (Array.size as)αβ) :
Equations
@[inline]
def Array.find? {α : Type} (as : Array α) (p : αBool) :
Equations
@[inline]
def Array.findSome? {α : Type u} {β : Type v} (as : Array α) (f : αOption β) :
Equations
@[inline]
def Array.findSome! {α : Type u} {β : Type v} [inst : Inhabited β] (a : Array α) (f : αOption β) :
β
Equations
@[inline]
def Array.findSomeRev? {α : Type u} {β : Type v} (as : Array α) (f : αOption β) :
Equations
@[inline]
def Array.findRev? {α : Type} (as : Array α) (p : αBool) :
Equations
@[inline]
def Array.findIdx? {α : Type u} (as : Array α) (p : αBool) :
Equations
def Array.findIdx?.loop {α : Type u} (as : Array α) (p : αBool) (i : Nat) (j : Nat) (inv : i + j = Array.size as) :
Equations
def Array.getIdx? {α : Type u} [inst : BEq α] (a : Array α) (v : α) :
Equations
@[inline]
def Array.any {α : Type u} (as : Array α) (p : αBool) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
@[inline]
def Array.all {α : Type u} (as : Array α) (p : αBool) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
def Array.contains {α : Type u} [inst : BEq α] (as : Array α) (a : α) :
Equations
def Array.elem {α : Type u} [inst : BEq α] (a : α) (as : Array α) :
Equations
def Array.reverse {α : Type u} (as : Array α) :
Equations
def Array.reverse.rev {α : Type u} (n : Nat) (mid : Nat) (as : Array α) (i : Nat) :
Equations
@[inline]
def Array.getEvenElems {α : Type u} (as : Array α) :
Equations
def Array.toList {α : Type u} (as : Array α) :
List α
Equations
instance Array.instReprArray {α : Type u} [inst : Repr α] :
Repr (Array α)
Equations
instance Array.instToStringArray {α : Type u} [inst : ToString α] :
Equations
def Array.append {α : Type u} (as : Array α) (bs : Array α) :
Equations
instance Array.instAppendArray {α : Type u} :
Equations
  • Array.instAppendArray = { append := Array.append }
def Array.appendList {α : Type u} (as : Array α) (bs : List α) :
Equations
instance Array.instHAppendArrayList {α : Type u} :
HAppend (Array α) (List α) (Array α)
Equations
  • Array.instHAppendArrayList = { hAppend := Array.appendList }
@[inline]
def Array.concatMapM {α : Type u} {m : Type u_1Type u_2} {β : Type u_1} [inst : Monad m] (f : αm (Array β)) (as : Array α) :
m (Array β)
Equations
@[inline]
def Array.concatMap {α : Type u} {β : Type u_1} (f : αArray β) (as : Array α) :
Equations
@[specialize]
def Array.isEqvAux {α : Type u_1} (a : Array α) (b : Array α) (hsz : Array.size a = Array.size b) (p : ααBool) (i : Nat) :
Equations
@[inline]
def Array.isEqv {α : Type u_1} (a : Array α) (b : Array α) (p : ααBool) :
Equations
instance Array.instBEqArray {α : Type u_1} [inst : BEq α] :
BEq (Array α)
Equations
  • Array.instBEqArray = { beq := fun a b => Array.isEqv a b BEq.beq }
@[inline]
def Array.filter {α : Type u_1} (p : αBool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
@[inline]
def Array.filterM {m : TypeType u_1} {α : Type} [inst : Monad m] (p : αm Bool) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
m (Array α)
Equations
@[specialize]
def Array.filterMapM {m : Type u_1Type 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
@[inline]
def Array.filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
@[specialize]
def Array.getMax? {α : Type u_1} (as : Array α) (lt : ααBool) :
Equations
@[inline]
def Array.partition {α : Type u_1} (p : αBool) (as : Array α) :
Array α × Array α
Equations
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
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
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
def Array.indexOfAux {α : Type u_1} [inst : BEq α] (a : Array α) (v : α) (i : Nat) :
Equations
def Array.indexOf? {α : Type u_1} [inst : BEq α] (a : Array α) (v : α) :
Equations
@[simp]
theorem Array.size_swap {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) :
@[simp]
theorem Array.size_pop {α : Type u_1} (a : Array α) :
def Array.popWhile {α : Type u_1} (p : αBool) (as : Array α) :
Equations
def Array.takeWhile {α : Type u_1} (p : αBool) (as : Array α) :
Equations
def Array.takeWhile.go {α : Type u_1} (p : αBool) (as : Array α) (i : Nat) (r : Array α) :
Equations
def Array.eraseIdxAux {α : Type u_1} (i : Nat) (a : Array α) :
Equations
def Array.feraseIdx {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) :
Equations
def Array.eraseIdx {α : Type u_1} (a : Array α) (i : Nat) :
Equations
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
def Array.eraseIdx' {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) :
{ r // Array.size r = Array.size a - 1 }
Equations
def Array.erase {α : Type u_1} [inst : BEq α] (as : Array α) (a : α) :
Equations
def Array.insertAtAux {α : Type u_1} (i : Nat) (as : Array α) (j : Nat) :
Equations
def Array.insertAt {α : Type u_1} (as : Array α) (i : Nat) (a : α) :
Equations

Insert element a at position i. Pre: i

def Array.toListLitAux {α : Type u_1} (a : Array α) (n : Nat) (hsz : Array.size a = n) (i : Nat) :
i Array.size aList αList α
Equations
def Array.toArrayLit {α : Type u_1} (a : Array α) (n : Nat) (hsz : Array.size a = n) :
Equations
theorem Array.toArrayLit_eq {α : Type u_1} (a : Array α) (n : Nat) (hsz : Array.size a = n) :
def Array.isPrefixOfAux {α : Type u_1} [inst : BEq α] (as : Array α) (bs : Array α) (hle : Array.size as Array.size bs) (i : Nat) :
Equations
def Array.isPrefixOf {α : Type u_1} [inst : BEq α] (as : Array α) (bs : Array α) :
Equations
def Array.allDiff {α : Type u_1} [inst : BEq α] (as : Array α) :
Equations
@[specialize]
def Array.zipWithAux {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :
Equations
@[inline]
def Array.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : αβγ) :
Equations
def Array.zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :
Array (α × β)
Equations
def Array.unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :
Array α × Array β
Equations
def Array.split {α : Type u_1} (as : Array α) (p : αBool) :
Array α × Array α
Equations