extract sublist from list

Stream: Is there code for X?

[Johan Commelin]

Does this exist already?

/-- Returns the sublist of `L` starting at index `m` of length `n`
(or shorter, if `L` is too short). -/
def list.extract {α : Sort*} (L : list α) (m n : ℕ) := ((L.split_at m).2.split_at n).1

#eval [0,1,2,3,4,5,6,7,8,9].extract 4 3 -- [4,5,6]

docs#list.slice will take a list L, and two nats n and m, and return the list constructed from L by dropping m elements starting from index n.
I'm interested in the part that is dropped. Is there already a function for that?

[Johan Commelin]

Is there a common name for this in list parlance in other languages?

[Scott Morrison]

I guess people usually just use list.take and list.drop.

[Scott Morrison]

#eval ([0,1,2,3,4,5,6,7,8,9].drop 4).take 3

[Kevin Buzzard]

This is some fundamental construction L[n,n+m] in python, right? What's it called in Haskell?

[Anne Baanen]

AFAICT, "slicing" is the near-universal word for Johan's operation, so docs#list.slice does exactly the opposite from almost everyone else.