### getLit #

source
@[reducible, inline]
abbrev Array.getLit {α : Type u} {n : Nat} (xs : Array α) (i : Nat) (h₁ : xs.size = n) (h₂ : i < n) :
α
Equations

- xs.getLit i h₁ h₂ = xs[i]

Instances For

source
theorem Array.extLit {α : Type u_1} {n : Nat} (xs ys : Array α) (hsz₁ : xs.size = n) (hsz₂ : ys.size = n) (h : ∀ (i : Nat) (hi : i < n), xs.getLit i hsz₁ hi = ys.getLit i hsz₂ hi) :
xs = ys
source
def Array.toListLitAux {α : Type u_1} (xs : Array α) (n : Nat) (hsz : xs.size = n) (i : Nat) :
i ≤ xs.size → List α → List α
Equations

- xs.toListLitAux n hsz 0 x_3 x = x
- xs.toListLitAux n hsz i.succ hi x = xs.toListLitAux n hsz i ⋯ (xs.getLit i hsz ⋯ :: x)

Instances For

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

- xs.toArrayLit n hsz = (xs.toListLitAux n hsz n ⋯ []).toArray

Instances For

source
theorem Array.toArrayLit_eq {α : Type u_1} (xs : Array α) (n : Nat) (hsz : xs.size = n) :
xs = xs.toArrayLit n hsz