How many lemmas are there about ListSlice?

Stream: mathlib4

[C7X]

ListSlice seems like a useful class, but unfortunately I'm having trouble finding many lemmas about it. How much has been written on ListSlice?

An example: a recent PR adds some new theorems about the class ListSlice, but on my machine (after updating mathlib4) I cannot access them. For example, if I type #check List.toList_mkSlice_roi, Lean gives me a lean.unknownIdentifier error.

[Yan Yablonovskiy 🇺🇦]

@loogle ListSlice

not sure how to loogle the core actually, didnt realise it was just mathlib. That PR is for lean4 not mathlib though

[loogle]

:search: ListSlice, List.toUnboundedSlice, and 24 more

[Markus Himmel]

The theorems in the linked PR will be part of Lean 4.27.0 which isn't released yet. That's why Loogle doesn't find them. Loogle does search Core, but the version of Core that mathlib uses at the moment, which right now is v4.26.0-rc2.