Documentation

Std.Data.Array.Init.Lemmas

While this file is currently empty, it is intended as a home for any lemmas which are required for definitions in Std.Data.Array.Basic, but which are not provided by Lean.