def Hex.Array.ofFn' {α : Type u} {n : Nat} (f : Fin n → α) : Array α

An Array.ofFn equivalent that reduces in the kernel under the module system.

Equations

• Hex.Array.ofFn' f = (List.ofFn f).toArray

def Hex.Vector.ofFn' {n : Nat} {α : Type u} (f : Fin n → α) : Vector α n

A Vector.ofFn equivalent that reduces in the kernel under the module system.

Equations

• Hex.Vector.ofFn' f = Vector.mk (List.ofFn f).toArray ⋯

@[simp]

theorem Hex.Array.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) : ofFn' f = Array.ofFn f

@[simp]

theorem Hex.Vector.ofFn'_eq_ofFn {n : Nat} {α : Type u} (f : Fin n → α) : ofFn' f = Vector.ofFn f

@[simp]

theorem Hex.Array.size_ofFn' {α : Type u} {n : Nat} (f : Fin n → α) : (ofFn' f).size = n

@[simp]

theorem Hex.Array.getElem_ofFn' {α : Type u} {n : Nat} (f : Fin n → α) (i : Nat) (h : i < (ofFn' f).size) : (ofFn' f)[i] = f ⟨i, ⋯⟩

@[simp]

theorem Hex.Vector.toArray_ofFn' {n : Nat} {α : Type u} (f : Fin n → α) : (ofFn' f).toArray = Array.ofFn' f

@[simp]

theorem Hex.Vector.getElem_ofFn' {n : Nat} {α : Type u} (f : Fin n → α) (i : Nat) (h : i < n) : (ofFn' f)[i] = f ⟨i, h⟩

@[csimp]

theorem Hex.Array.ofFn'_eq_ofFn' : @ofFn' = @Array.ofFn

Compiled code uses the core Array.ofFn, which fills an array of known capacity instead of building a List first. The List route exists only so that the kernel can reduce it.

@[csimp]

theorem Hex.Vector.ofFn'_eq_ofFn' : @ofFn' = @Vector.ofFn

The Hex.Vector.ofFn' analogue of Hex.Array.ofFn'_eq_ofFn'.