@[extern lean_mk_array]

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

@[simp]

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

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

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

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

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

@[extern lean_array_uget]

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

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.

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

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

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

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

@[inline, reducible]

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

@[simp]

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

@[simp]

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

@[extern lean_array_uset]

def Array.uset {α : Type u} (a : Array α) (i : USize) (v : α) (h : USize.toNat i < Array.size a) : 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.

@[extern lean_array_fswap]

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

@[extern lean_array_swap]

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

@[inline]

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

@[inline]

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

@[extern lean_array_pop]

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

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

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)

@[inline]

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

@[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 α)

@[inline]

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

@[inline]

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

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

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

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

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

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

@[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 (Array.size as)) : m β

See comment at forInUnsafe

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

@[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 (Array.size as)) : m β

Reference implementation for foldlM

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

@[inline]

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

See comment at forInUnsafe

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

@[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 (Array.size as)) (stop : optParam Nat 0) : m β

Reference implementation for foldrM

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 ≤ 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

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

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

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

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 < Array.size as then do let __do_lift ← f as[i] Array.mapM.map f as (i + 1) (Array.push r __do_lift) else pure r

@[inline]

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

@[specialize #[]]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[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 (Array.size as)) : m Bool

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

@[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 (Array.size as)) : m Bool

def Array.anyM.loop {α : Type u} {m : Type → Type w} [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.

@[inline]

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

@[inline]

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

@[specialize #[]]

def Array.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) (i : Nat) : i ≤ 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

@[inline]

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

@[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 (Array.size as)) : m PUnit

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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.

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

@[inline]

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

@[inline]

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

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

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

@[inline]

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

@[export lean_array_to_list]

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

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

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

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

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

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

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

@[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 β)

@[inline]

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

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

@[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_fun this := (_ : i < Array.size b); p a[i] b[i] && Array.isEqvAux a b hsz p (i + 1) else true

@[inline]

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

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

@[inline]

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

@[inline]

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

@[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 (Array.size as)) : m (Array β)

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

@[specialize #[]]

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

@[inline]

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

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), a[i] = b[i]) : 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} [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

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

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

@[simp]

theorem Array.size_pop {α : Type u_1} (a : Array α) : Array.size (Array.pop a) = Array.size a - 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 α

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

Equations

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

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

Equations

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

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

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.

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

Equations

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

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

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

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

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

def Array.eraseIdx' {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) : { r // Array.size r = Array.size a - 1 }

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

@[inline]

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

Insert element a at position i.

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

Equations

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

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.

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_3 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)

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

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

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

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 : Array.size as = n) : as = Array.toArrayLit as n hsz

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

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

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

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 α.

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

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

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

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

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