Loogle!

Result

Found 115 declarations mentioning ListSlice.

• ListSlice 📋 Init.Data.Slice.List.Basic
  (α : Type u) : Type u
• List.toUnboundedSlice 📋 Init.Data.Slice.List.Basic
  {α : Type u} (as : List α) (start : ℕ) : ListSlice α
• instSliceableListNatListSlice 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rcc.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_1 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rco.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_2 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rci.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_3 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Roc.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_4 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Roo.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_5 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Roi.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_6 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Ric.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_7 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rio.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListNatListSlice_8 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rii.Sliceable (List α) ℕ (ListSlice α)
• instSliceableListSliceNat 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rcc.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_1 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rco.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_2 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rci.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_3 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Roc.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_4 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Roo.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_5 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Roi.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_6 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Ric.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_7 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rio.Sliceable (ListSlice α) ℕ (ListSlice α)
• instSliceableListSliceNat_8 📋 Init.Data.Slice.List.Basic
  {α : Type u} : Std.Rii.Sliceable (ListSlice α) ℕ (ListSlice α)
• List.toSlice 📋 Init.Data.Slice.List.Basic
  {α : Type u} (as : List α) (start stop : ℕ) : ListSlice α
• List.instAppendListSlice 📋 Init.Data.Slice.List.Iterator
  {α : Type u} : Append (ListSlice α)
• List.instReprListSlice 📋 Init.Data.Slice.List.Iterator
  {α : Type u} [Repr α] : Repr (ListSlice α)
• List.instToStringListSlice 📋 Init.Data.Slice.List.Iterator
  {α : Type u} [ToString α] : ToString (ListSlice α)
• List.ListSlice.repr 📋 Init.Data.Slice.List.Iterator
  {α : Type u} [Repr α] (s : ListSlice α) : Std.Format
• instForInListSliceOfMonad 📋 Init.Data.Slice.List.Iterator
  {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (ListSlice α) α
• ListSlice.mkSlice_rii 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} : Std.Rii.Sliceable.mkSlice xs *...* = xs
• List.size_mkSlice_rii 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} : Std.Slice.size (Std.Rii.Sliceable.mkSlice xs *...*) = xs.length
• List.size_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi xs.length
• List.mkSlice_rii_eq_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} : Std.Rii.Sliceable.mkSlice xs *...* = Std.Rci.Sliceable.mkSlice xs 0...*
• ListSlice.size_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi (Std.Slice.size xs)
• List.size_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = xs.length - lo
• List.mkSlice_rio_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
• ListSlice.mkSlice_ric_eq_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rcc.Sliceable.mkSlice xs 0...=hi
• ListSlice.mkSlice_rio_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
• ListSlice.size_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.size xs - lo
• List.size_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi xs.length - lo
• List.size_mkSlice_ric 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) xs.length
• List.mkSlice_ric_eq_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
• List.mkSlice_roi_eq_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
• ListSlice.mkSlice_ric_eq_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
• ListSlice.mkSlice_roi_eq_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*
• ListSlice.size_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi (Std.Slice.size xs) - lo
• ListSlice.size_mkSlice_ric 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) (Std.Slice.size xs)
• List.mkSlice_rcc_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
• List.mkSlice_roc_eq_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
• List.mkSlice_roo_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : (Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
• List.size_mkSlice_roi 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = xs.length - (lo + 1)
• ListSlice.mkSlice_rcc_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
• ListSlice.mkSlice_roc_eq_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rcc.Sliceable.mkSlice xs (lo + 1)...=hi
• ListSlice.mkSlice_roc_eq_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
• ListSlice.mkSlice_roo_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : (Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
• ListSlice.size_eq_length_toList 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} : Std.Slice.size xs = (Std.Slice.toList xs).length
• List.mkSlice_ric_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rco.Sliceable.mkSlice xs 0...hi + 1
• ListSlice.mkSlice_ric_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rco.Sliceable.mkSlice xs 0...hi + 1
• ListSlice.size_mkSlice_roi 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.size xs - (lo + 1)
• List.toList_mkSlice_rii 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} : Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = xs
• List.size_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) xs.length - lo
• List.size_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi xs.length - (lo + 1)
• List.toArray_mkSlice_rii 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} : Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = xs.toArray
• ListSlice.size_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) (Std.Slice.size xs) - lo
• ListSlice.size_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi (Std.Slice.size xs) - (lo + 1)
• List.toList_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo xs
• List.toList_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi xs
• List.mkSlice_roc_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi + 1
• List.toArray_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (List.drop lo xs).toArray
• List.toArray_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (List.take hi xs).toArray
• ListSlice.mkSlice_roc_eq_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi + 1
• List.toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi xs)
• List.toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (List.drop lo (List.take hi xs)).toArray
• List.size_mkSlice_roc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) xs.length - (lo + 1)
• ListSlice.size_mkSlice_roc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) (Std.Slice.size xs) - (lo + 1)
• List.toList_mkSlice_ric 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) xs
• List.toList_mkSlice_roi 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) xs
• ListSlice.toList_eq 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} : Std.Slice.toList xs = match xs.internalRepresentation.stop with | some stop => List.take stop xs.internalRepresentation.list | none => xs.internalRepresentation.list
• List.toArray_mkSlice_ric 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {hi : ℕ} : Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (List.take (hi + 1) xs).toArray
• List.toArray_mkSlice_roi 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (List.drop (lo + 1) xs).toArray
• List.toList_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) xs)
• List.toList_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi xs)
• List.toArray_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (List.drop lo (List.take (hi + 1) xs)).toArray
• List.toArray_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (List.drop (lo + 1) (List.take hi xs)).toArray
• ListSlice.toArray_toList 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} : (Std.Slice.toList xs).toArray = Std.Slice.toArray xs
• ListSlice.toList_toArray 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} : (Std.Slice.toArray xs).toList = Std.Slice.toList xs
• List.toList_mkSlice_roc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = List.drop (lo + 1) (List.take (hi + 1) xs)
• List.toArray_mkSlice_roc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo hi : ℕ} : Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (List.drop (lo + 1) (List.take (hi + 1) xs)).toArray
• ListSlice.toList_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = List.drop lo (Std.Slice.toList xs)
• ListSlice.toList_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi (Std.Slice.toList xs)
• ListSlice.toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (Std.Slice.toArray xs).extract lo hi
• ListSlice.toArray_mkSlice_rio 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (Std.Slice.toArray xs).extract 0 hi
• ListSlice.toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi (Std.Slice.toList xs))
• List.toArray_mkSlice_rci_eq_toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...xs.length)
• List.toArray_mkSlice_roi_eq_toArray_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...xs.length)
• List.toList_mkSlice_rci_eq_toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...xs.length)
• List.toList_mkSlice_roi_eq_toList_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...xs.length)
• ListSlice.toList_mkSlice_ric 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) (Std.Slice.toList xs)
• ListSlice.toList_mkSlice_roi 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) (Std.Slice.toList xs)
• List.toArray_mkSlice_rii_eq_toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} : Std.Slice.toArray (Std.Rii.Sliceable.mkSlice xs *...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs 0...xs.length)
• List.toList_mkSlice_rii_eq_toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} : Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs 0...xs.length)
• ListSlice.toArray_mkSlice_rci_eq_toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...Std.Slice.size xs)
• ListSlice.toArray_mkSlice_roi_eq_toArray_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...Std.Slice.size xs)
• ListSlice.toList_mkSlice_rci_eq_toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...Std.Slice.size xs)
• ListSlice.toList_mkSlice_roi_eq_toList_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...Std.Slice.size xs)
• ListSlice.toArray_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (Std.Slice.toArray xs).extract lo (hi + 1)
• ListSlice.toArray_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...hi) = (Std.Slice.toArray xs).extract (lo + 1) hi
• ListSlice.toArray_mkSlice_ric 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {hi : ℕ} : Std.Slice.toArray (Std.Ric.Sliceable.mkSlice xs *...=hi) = (Std.Slice.toArray xs).extract 0 (hi + 1)
• ListSlice.toList_mkSlice_rcc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) (Std.Slice.toList xs))
• ListSlice.toList_mkSlice_roo 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...hi) = List.drop (lo + 1) (List.take hi (Std.Slice.toList xs))
• List.toArray_mkSlice_roi_eq_toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo + 1)...xs.length)
• List.toList_mkSlice_roi_eq_toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : List α} {lo : ℕ} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs (lo + 1)...xs.length)
• ListSlice.toArray_mkSlice_roi_eq_toArray_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs (lo + 1)...Std.Slice.size xs)
• ListSlice.toList_mkSlice_roi_eq_toList_mkSlice_rco 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs (lo + 1)...Std.Slice.size xs)
• ListSlice.toArray_mkSlice_roc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (Std.Slice.toArray xs).extract (lo + 1) (hi + 1)
• ListSlice.toList_mkSlice_roc 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ} : Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = List.drop (lo + 1) (List.take (hi + 1) (Std.Slice.toList xs))
• ListSlice.toArray_mkSlice_rci 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (Std.Slice.toArray xs).extract lo
• ListSlice.toArray_mkSlice_roi 📋 Init.Data.Slice.List.Lemmas
  {α : Type u_1} {xs : ListSlice α} {lo : ℕ} : Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (Std.Slice.toArray xs).extract (lo + 1)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 401c76f serving mathlib revision b87935d