Def Array.range

Modification history

2022-09-04 16:26

Mathlib/Data/Array/Defs.lean

feat: depend on std4 (#397)

Deleted Array.range View on Github →

2022-06-13 19:31

Mathlib/Data/Array/Defs.lean

feat: port misc linters (#276)

Modified Array.range View on Github →

2021-12-09 16:23

Mathlib/Data/Array/Defs.lean

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

Added Array.range View on Github →