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'.

def Hex.Array.map' {α : Type u} {β : Type v} (f : α → β) (a : Array α) : Array β

An Array.map equivalent that reduces in the kernel under the module system: core Array.map's implementation loop is not exposed, so (a.map f) stalls downstream exactly like Array.ofFn. Retire once <https://github.com/leanprover/lean4/pull/14996> reaches the pinned toolchain.

Equations

• Hex.Array.map' f a = (List.map f a.toList).toArray

@[simp]

theorem Hex.Array.map'_eq_map {α : Type u} {β : Type v} (f : α → β) (a : Array α) : map' f a = Array.map f a

@[simp]

theorem Hex.Array.size_map' {α : Type u} {β : Type v} (f : α → β) (a : Array α) : (map' f a).size = a.size

@[simp]

theorem Hex.Array.getElem_map' {α : Type u} {β : Type v} (f : α → β) (a : Array α) (i : Nat) (h : i < (map' f a).size) : (map' f a)[i] = f a[i]

@[csimp]

theorem Hex.Array.map'_eq_map' : @map' = @Array.map

Compiled code uses the core Array.map, which writes into an array in place when uniquely referenced; the List route exists only so that the kernel can reduce it.

def Hex.Array.zipWith' {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) : Array γ

An Array.zipWith equivalent that reduces in the kernel under the module system: core Array.zipWith runs its zipWithMAux loop by well-founded recursion, so (Array.zipWith f a b) stalls downstream exactly like Array.map. Retire once core exposes a structurally recursive implementation.

Equations

• Hex.Array.zipWith' f a b = (List.zipWith f a.toList b.toList).toArray

@[simp]

theorem Hex.Array.zipWith'_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) : zipWith' f a b = Array.zipWith f a b

@[simp]

theorem Hex.Array.size_zipWith' {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) : (zipWith' f a b).size = min a.size b.size

@[simp]

theorem Hex.Array.getElem_zipWith' {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : Array α) (b : Array β) (i : Nat) (h : i < (zipWith' f a b).size) : (zipWith' f a b)[i] = f a[i] b[i]

@[csimp]

theorem Hex.Array.zipWith'_eq_zipWith' : @zipWith' = @Array.zipWith

Compiled code uses the core Array.zipWith, which writes into an array of known capacity; the List route exists only so that the kernel can reduce it.