getLit

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

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

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)

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

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

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

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