@[extern lean_mk_array]
Instances For
@[simp]
instance
Array.instGetElemArrayUSizeLtNatInstLTNatToNatSize
{α : Type u}
:
GetElem (Array α) USize α fun xs i => USize.toNat i < Array.size xs
@[inline, reducible]
abbrev
Array.getLit
{α : Type u}
{n : Nat}
(a : Array α)
(i : Nat)
(h₁ : Array.size a = n)
(h₂ : i < n)
:
α
Instances For
@[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
.
Instances For
@[extern lean_array_fswap]
def
Array.swap
{α : Type u}
(a : Array α)
(i : Fin (Array.size a))
(j : Fin (Array.size a))
:
Array α
Instances For
@[inline]
Instances For
Equations
- Array.shrink.loop 0 x = x
- Array.shrink.loop (Nat.succ n) x = Array.shrink.loop n (Array.pop x)
Instances For
@[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.
Instances For
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
Instances For
@[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
Instances For
@[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
Instances For
@[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
Instances For
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
Instances For
@[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
Instances For
@[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
Instances For
@[inline]
def
Array.foldl
{α : Type u}
{β : Type v}
(f : β → α → β)
(init : β)
(as : Array α)
(start : optParam Nat 0)
(stop : optParam Nat (Array.size as))
:
β
Instances For
@[inline]
def
Array.foldr
{α : Type u}
{β : Type v}
(f : α → β → β)
(init : β)
(as : Array α)
(start : optParam Nat (Array.size as))
(stop : optParam Nat 0)
:
β
Instances For
@[inline]
def
Array.mapIdx
{α : Type u}
{β : Type v}
(as : Array α)
(f : Fin (Array.size as) → α → β)
:
Array β
Instances For
@[export lean_array_to_list]
Instances For
@[specialize #[]]
def
Array.isEqvAux
{α : Type u_1}
(a : Array α)
(b : Array α)
(hsz : Array.size a = Array.size b)
(p : α → α → Bool)
(i : Nat)
:
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
Instances For
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
Instances For
Instances For
@[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]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
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.
Instances For
def
Array.eraseIdx'
{α : Type u_1}
(a : Array α)
(i : Fin (Array.size a))
:
{ r // Array.size r = Array.size a - 1 }
Instances For
@[inline]
Insert element a
at position i
.
Instances For
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.
Instances For
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)
Instances For
Instances For
theorem
Array.toArrayAux_eq
{α : Type u_1}
(as : List α)
(acc : Array α)
:
(List.toArrayAux as acc).data = acc.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)
:
Equations
- One or more equations did not get rendered due to their size.