fix: expose `Array.back`, `back!`, and `back?`

This PR marks `Array.back`, `Array.back!`, and `Array.back?` as `@[expose]`, so that in a downstream module their bodies are available for definitional reduction. Previously `decide` (and even `decide +kernel`) could not evaluate goals such as `#[1, 2, 3].back? = some 3` from another module, even though the `getElem?`/`size` accessors these functions are defined in terms of, and the neighbouring `Array.singleton`, are already exposed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

src/Init/Data/Array/Basic.lean

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 3104770..b38a623 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -380,7 +380,7 @@
 Safer alternatives include `Array.back`, which requires a proof the array is non-empty, and
 `Array.back?`, which returns an `Option`.
 -/
-@[inline]
+@[inline, expose]
 def back! [Inhabited α] (xs : Array α) : α :=
   xs[xs.size - 1]!
 
@@ -390,7 +390,7 @@
 See `Array.back!` for the version that panics if the array is empty, or `Array.back?` for the
 version that returns an option.
 -/
-@[inline]
+@[inline, expose]
 def back (xs : Array α) (h : 0 < xs.size := by get_elem_tactic) : α :=
   xs[xs.size - 1]'(Nat.sub_one_lt_of_lt h)
 
@@ -400,7 +400,7 @@
 See `Array.back!` for the version that panics if the array is empty, or `Array.back` for the version
 that requires a proof the array is non-empty.
 -/
-@[inline]
+@[inline, expose]
 def back? (xs : Array α) : Option α :=
   xs[xs.size - 1]?
 

tests/elab/exposeArrayBack.lean

diff --git a/tests/elab/exposeArrayBack.lean b/tests/elab/exposeArrayBack.lean
new file mode 100644
index 0000000..6543247
--- /dev/null
+++ b/tests/elab/exposeArrayBack.lean
@@ -0,0 +1,19 @@
+module
+
+/-!
+`Array.back`, `Array.back!`, and `Array.back?` are `@[expose]`, so a
+downstream `module` can reduce them under `decide` (and the kernel), exactly
+like the `getElem?`/`size` accessors they are defined in terms of. Without
+the attribute their bodies do not cross the module boundary and the `decide`
+calls below get stuck on the unreduced application.
+-/
+
+-- Baseline: the accessors `back?` is built from already reduce.
+example : (#[1, 2, 3] : Array Nat)[2]? = some 3 := by decide
+example : (#[1, 2, 3] : Array Nat).size = 3 := by decide
+
+-- The `back` family must reduce too.
+example : (#[1, 2, 3] : Array Nat).back? = some 3 := by decide
+example : (#[1, 2, 3] : Array Nat).back? = some 3 := by decide +kernel
+example : (#[1, 2, 3] : Array Nat).back! = 3 := by decide
+example : (#[1, 2, 3] : Array Nat).back = 3 := by decide