Bootstrapping properties of Arrays #
@[simp]
theorem
Array.size_ofFn_go
{α : Type u_1}
{n : Nat}
(f : Fin n → α)
(i : Nat)
(acc : Array α)
:
Array.size (Array.ofFn.go f i acc) = Array.size acc + (n - i)
@[simp]
theorem
Array.getElem_ofFn_go
{n : Nat}
{α : Type u_1}
(f : Fin n → α)
(i : Nat)
{acc : Array α}
{k : Nat}
(hki : k < n)
(hin : i ≤ n)
(hi : i = Array.size acc)
(hacc : ∀ (j : Nat) (hj : j < Array.size acc), acc[j] = f { val := j, isLt := ⋯ })
:
(Array.ofFn.go f i acc)[k] = f { val := k, isLt := hki }
@[simp]
theorem
Array.getElem_ofFn
{n : Nat}
{α : Type u_1}
(f : Fin n → α)
(i : Nat)
(h : i < Array.size (Array.ofFn f))
:
(Array.ofFn f)[i] = f { val := i, isLt := ⋯ }