chore: upstream Array.reduceOption

2026-03-17 18:34:06 +00:00 · 2024-10-18 11:21:17 +11:00
1 changed files with 7 additions and 1 deletions
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -817,9 +817,15 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=

 /-! ## Auxiliary functions used in metaprogramming.

-We do not intend to provide verification theorems for these functions.
+We do not currently intend to provide verification theorems for these functions.
 -/

+/- ### reduceOption -/
+
+/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
+@[inline] def reduceOption (as : Array (Option α)) : Array α :=
+  as.filterMap id
+
 /-! ### eraseReps -/

 /--