diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 7d58dee5983a..3b60fdaf338d 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -328,7 +328,7 @@ Examples:
  * `Array.ofFn (n := 3) toString = #["0", "1", "2"]`
  * `Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]`
 -/
-def ofFn {n} (f : Fin n → α) : Array α := go (emptyWithCapacity n) n (Nat.le_refl n) where
+@[expose] def ofFn {n} (f : Fin n → α) : Array α := go (emptyWithCapacity n) n (Nat.le_refl n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f acc i h = acc ++ #[f (n - i), ..., f(n - 1)]` -/
   go (acc : Array α) : (i : Nat) → i ≤ n → Array α
   | i + 1, h =>
diff --git a/tests/elab/array_offn_module.lean b/tests/elab/array_offn_module.lean
new file mode 100644
index 000000000000..2ddc5366196c
--- /dev/null
+++ b/tests/elab/array_offn_module.lean
@@ -0,0 +1,9 @@
+module
+
+/-!
+Tests kernel reduction of `Array.ofFn` across a module boundary.
+-/
+
+example : (Array.ofFn (n := 3) (fun i => i.val)).size = 3 := by rfl
+example : Array.ofFn (n := 3) (fun i => i.val) = #[0, 1, 2] := by rfl
+example : Vector.ofFn (n := 3) (fun i => i.val) = #v[0, 1, 2] := by rfl