Def Array.reduceOption

Modification history

2022-09-04 16:26

Mathlib/Data/Array/Defs.lean

feat: depend on std4 (#397)

Deleted Array.reduceOption View on Github →

2021-12-09 16:23

Mathlib/Data/Array/Defs.lean

feat(*): some auxiliary definitions for toAdditive (#112) …

Added Array.reduceOption View on Github →