@[extern lean_mk_array]

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

Equations

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Array.singleton v = mkArray 1 v

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

Equations

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

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

Equations

• Array.instGetElemArrayUSizeLtNatInstLTNatToNatSize = { getElem := fun xs i h => Array.uget xs i h }

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

• Array.getLit a i h₁ h₂ = let_fun this := (_ : i < Array.size a); a[i]

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

Equations

• Array.uset a i v h = Array.set a { val := USize.toNat i, isLt := h } v

@[extern lean_array_fswap]

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

Equations

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

@[extern lean_array_swap]

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

Equations

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

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

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

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

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

Equations

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

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} [inst : 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} [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

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

@[inline]

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

Equations

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

@[inline]

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

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

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

@[implemented_by Array.forInUnsafe]

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

Reference implementation for forIn

Equations

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

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

instance Array.instForInArray {α : Type u} {m : Type u_1 → Type 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 v → Type w} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) : m β

See comment at forInUnsafe

Equations

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

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

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

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

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

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

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

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

@[inline]

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

See comment at forInUnsafe

Equations

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

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

@[implemented_by Array.mapMUnsafe]

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

Reference implementation for mapM

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)

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

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

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

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

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

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

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

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

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.

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

@[specialize #[]]

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

Equations

• Array.findRevM? as p = Array.findSomeRevM? as 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} [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

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

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

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

@[inline]

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

Equations

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

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

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} [inst : BEq α] (a : Array α) (v : α) : Option Nat

Equations

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

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

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

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)

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

Equations

• Array.elem a as = Array.contains as 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 α

Equations

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

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

Equations

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

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

Equations

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

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)

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

Equations

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

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

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

Equations

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

@[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 __do_lift ← f a pure (bs ++ __do_lift)) #[] as 0 (Array.size as)

@[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) #[] as 0 (Array.size as)

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

Equations

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

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

Equations

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

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

@[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 __do_lift ← p a if __do_lift = true then pure (Array.push r a) else pure r) #[] as start stop

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

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

@[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 := as[0]; some (Array.foldl (fun best a => if lt best a = true then a else best) a0 as 1 (Array.size as)) 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₁ : 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} [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

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

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

Equations

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

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 α

Equations

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

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 α

Equations

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

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

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 }

Equations

• Array.eraseIdx' a i = Array.eraseIdxSzAux a (i.val + 1) a (_ : Array.size a = Array.size a)

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

@[inline]

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

Insert element a at position i.

Equations

• Array.insertAt as i a = let j := Array.size as; let as := Array.push as a; Array.insertAt.loop as i as { val := j, isLt := (_ : Array.size as < Array.size (Array.push as a)) }

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.

Equations

• One or more equations did not get rendered due to their 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 α

Equations

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

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

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

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

Equations

• Array.allDiff as = Array.allDiffAux as 0

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

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

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

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.

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)