Documentation

Mathlib.Data.List.InsertNth

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.