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