This is a stub file for importing Mathlib.Data.List.InsertNth
,
which has been renamed to Mathlib.Data.List.InsertIdx
.
This file can be removed once the deprecation for List.insertNth
is removed.
This is a stub file for importing Mathlib.Data.List.InsertNth
,
which has been renamed to Mathlib.Data.List.InsertIdx
.
This file can be removed once the deprecation for List.insertNth
is removed.