getLit

@[reducible, inline]

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

Equations

• a.getLit i h₁ h₂ = a[i]

theorem Array.extLit {α : Type u_1} {n : Nat} (a b : Array α) (hsz₁ : a.size = n) (hsz₂ : b.size = n) (h : ∀ (i : Nat) (hi : i < n), a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b

def Array.toListLitAux {α : Type u_1} (a : Array α) (n : Nat) (hsz : a.size = n) (i : Nat) : i ≤ a.size → List α → List α

Equations

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

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

Equations

• a.toArrayLit n hsz = (a.toListLitAux n hsz n ⋯ []).toArray

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

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

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