Documentation

Init.Data.Array.TakeDrop

theorem Array.exists_of_uset {α : Type u_1} (self : Array α) (i : USize) (d : α) (h : i.toNat < self.size) :
∃ (l₁ : List α), ∃ (l₂ : List α), self.toList = l₁ ++ self[i] :: l₂ l₁.length = i.toNat (self.uset i d h).toList = l₁ ++ d :: l₂