fix

src/Init/Data/Array/QSort/Basic.lean

@@ -55,7 +55,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
 /--
 In-place quicksort.
 
-`qsort as lt lo hi` sorts the subarray `as[lo...=hi]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
     (lo := 0) (hi := as.size - 1) : Array α :=
@@ -65,7 +65,7 @@ In-place quicksort.
       let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
       if h₂ : mid ≥ hi then
         -- This only occurs when `hi ≤ lo`,
-        -- and thus `as[lo...(hi+1)]` is trivially already sorted.
+        -- and thus `as[lo:hi+1]` is trivially already sorted.
         as
       else
         -- Otherwise, we recursively sort the two subarrays.

src/Init/Data/Array/Subarray.lean

@@ -82,7 +82,7 @@ def size (s : Subarray α) : Nat :=
 
 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
   let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
-  simp only [size, ge_iff_le]
+  simp [size]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
 
@@ -95,7 +95,7 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
   have : s.start + i.val < s.array.size := by
    apply Nat.lt_of_lt_of_le _ s.stop_le_array_size
    have := i.isLt
-   simp only [size] at this
+   simp [size] at this
    rw [Nat.add_comm]
    exact Nat.add_lt_of_lt_sub this
   s.array[s.start + i.val]

src/Init/Data/ByteArray/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Array.Subarray
 import Init.Data.UInt.Basic
 import all Init.Data.UInt.BasicAux
 import Init.Data.Option.Basic

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -37,6 +37,7 @@ Relation that needs to be well-formed in order for a loop over an iterator to te
 It is assumed that the `plausible_forInStep` predicate relates the input and output of the
 stepper function.
 -/
+@[expose]
 def IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop)
     (p' p : IterM (α := α) m β × γ) : Prop :=
@@ -46,6 +47,7 @@ def IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Itera
 /--
 Asserts that `IteratorLoop.rel` is well-founded.
 -/
+@[expose]
 def IteratorLoop.WellFounded (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop) : Prop :=
     _root_.WellFounded (IteratorLoop.rel α m plausible_forInStep)
@@ -106,19 +108,21 @@ class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [
 end Typeclasses
 
 /-- Internal implementation detail of the iterator library. -/
+@[expose]
 def IteratorLoop.WFRel {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
     (_wf : WellFounded α m plausible_forInStep) :=
   IterM (α := α) m β × γ
 
 /-- Internal implementation detail of the iterator library. -/
+@[expose]
 def IteratorLoop.WFRel.mk {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
     (wf : WellFounded α m plausible_forInStep) (it : IterM (α := α) m β) (c : γ) :
     IteratorLoop.WFRel wf :=
   (it, c)
 
-private instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
     (wf : IteratorLoop.WellFounded α m plausible_forInStep) :
     WellFoundedRelation (IteratorLoop.WFRel wf) where

src/Init/Data/Range/Polymorphic/Basic.lean

@@ -6,10 +6,34 @@ Authors: Paul Reichert
 module
 
 prelude
-import Init.Data.Range.Polymorphic.PRange
+import Init.Data.Range.Polymorphic.RangeIterator
+import Init.Data.Iterators.Combinators.Attach
+
+open Std.Iterators
 
 namespace Std.PRange
 
+/--
+Internal function that constructs an iterator for a `PRange`. This is an internal function.
+Use `PRange.iter` instead, which requires importing `Std.Data.Iterators`.
+-/
+@[always_inline, inline]
+def Internal.iter {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    (r : PRange ⟨sl, su⟩ α) : Iter (α := RangeIterator su α) α :=
+  ⟨⟨BoundedUpwardEnumerable.init? r.lower, r.upper⟩⟩
+
+/--
+Returns the elements of the given range as a list in ascending order, given that ranges of the given
+type and shape support this function and the range is finite.
+-/
+@[always_inline, inline]
+def toList {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α]
+    (r : PRange ⟨sl, su⟩ α)
+    [Iterator (RangeIterator su α) Id α] [Finite (RangeIterator su α) Id]
+    [IteratorCollect (RangeIterator su α) Id Id] : List α :=
+  PRange.Internal.iter r |>.toList
+
 /--
 This typeclass provides support for the `PRange.size` function.
 
@@ -46,6 +70,25 @@ class LawfulRangeSize (su : BoundShape) (α : Type u) [UpwardEnumerable α]
       (h' : UpwardEnumerable.succ? init = some a) :
       RangeSize.size upperBound init = RangeSize.size upperBound a + 1
 
+/--
+Iterators for ranges implementing `RangeSize` support the `size` function.
+-/
+instance [RangeSize su α] [UpwardEnumerable α] [SupportsUpperBound su α] :
+    IteratorSize (RangeIterator su α) Id where
+  size it := match it.internalState.next with
+    | none => pure (.up 0)
+    | some next => pure (.up (RangeSize.size it.internalState.upperBound next))
+
+/--
+Returns the number of elements contained in the given range, given that ranges of the given
+type and shape support this function.
+-/
+@[always_inline, inline]
+def size {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α] (r : PRange ⟨sl, su⟩ α)
+    [IteratorSize (RangeIterator su α) Id] : Nat :=
+  PRange.Internal.iter r |>.size
+
 /--
 Checks whether the range contains any value.
 
@@ -58,6 +101,56 @@ def isEmpty {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
     [SupportsUpperBound su α] (r : PRange ⟨sl, su⟩ α) : Bool :=
   (BoundedUpwardEnumerable.init? r.lower).all (! SupportsUpperBound.IsSatisfied r.upper ·)
 
+section Iterator
+
+theorem Internal.isPlausibleIndirectOutput_iter_iff {sl su α}
+    [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsLowerBound sl α] [SupportsUpperBound su α]
+    [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLowerBound sl α]
+    {r : PRange ⟨sl, su⟩ α} {a : α} :
+    (PRange.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r := by
+  rw [RangeIterator.isPlausibleIndirectOutput_iff]
+  constructor
+  · rintro ⟨n, hn, hu⟩
+    refine ⟨?_, hu⟩
+    rw [LawfulUpwardEnumerableLowerBound.isSatisfied_iff]
+    cases hr : (PRange.Internal.iter r).internalState.next
+    · simp [hr] at hn
+    · rw [hr, Option.bind_some] at hn
+      exact ⟨_, hr, n, hn⟩
+  · rintro ⟨hl, hu⟩
+    rw [LawfulUpwardEnumerableLowerBound.isSatisfied_iff] at hl
+    obtain ⟨_, hr, n, hn⟩ := hl
+    exact ⟨n, by simp [PRange.Internal.iter, hr, hn], hu⟩
+
+theorem RangeIterator.upwardEnumerableLe_of_isPlausibleIndirectOutput {su α}
+    [UpwardEnumerable α] [SupportsUpperBound su α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α]
+    {it : Iter (α := RangeIterator su α) α} {out : α}
+    (hout : it.IsPlausibleIndirectOutput out) :
+    ∃ a, it.internalState.next = some a ∧ UpwardEnumerable.LE a out := by
+  have ⟨a, ha⟩ := Option.isSome_iff_exists.mp <|
+    RangeIterator.isSome_next_of_isPlausibleIndirectOutput hout
+  refine ⟨a, ha, ?_⟩
+  simp only [isPlausibleIndirectOutput_iff, ha, Option.bind_some, exists_and_right] at hout
+  exact hout.1
+
+@[no_expose]
+instance {sl su α m} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsLowerBound sl α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
+    [Monad m] [Finite (RangeIterator su α) Id] :
+    ForIn' m (PRange ⟨sl, su⟩ α) α inferInstance where
+  forIn' r init f := by
+    haveI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
+    haveI := Iter.instForIn' (α := RangeIterator su α) (β := α) (n := m)
+    refine ForIn'.forIn' (α := α) (PRange.Internal.iter r) init (fun a ha acc => f a ?_ acc)
+    simp only [Membership.mem] at ha
+    rwa [PRange.Internal.isPlausibleIndirectOutput_iter_iff] at ha
+
+end Iterator
+
 theorem le_upper_of_mem {sl α} [LE α] [DecidableLE α] [SupportsLowerBound sl α]
     {a : α} {r : PRange ⟨sl, .closed⟩ α} (h : a ∈ r) : a ≤ r.upper :=
   h.2

src/Init/Data/Range/Polymorphic/Iterators.lean

@@ -1,151 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-import Init.Data.Range.Polymorphic.RangeIterator
-import Init.Data.Range.Polymorphic.Basic
-import Init.Data.Iterators.Combinators.Attach
-
-open Std.Iterators
-
-namespace Std.PRange
-
-/--
-Internal function that constructs an iterator for a `PRange`. This is an internal function.
-Use `PRange.iter` instead, which requires importing `Std.Data.Iterators`.
--/
-@[always_inline, inline]
-def Internal.iter {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
-    (r : PRange ⟨sl, su⟩ α) : Iter (α := RangeIterator su α) α :=
-  ⟨⟨BoundedUpwardEnumerable.init? r.lower, r.upper⟩⟩
-
-/--
-Returns the elements of the given range as a list in ascending order, given that ranges of the given
-type and shape support this function and the range is finite.
--/
-@[always_inline, inline]
-def toList {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
-    [SupportsUpperBound su α]
-    (r : PRange ⟨sl, su⟩ α)
-    [Iterator (RangeIterator su α) Id α] [Finite (RangeIterator su α) Id]
-    [IteratorCollect (RangeIterator su α) Id Id] : List α :=
-  PRange.Internal.iter r |>.toList
-
-/--
-Iterators for ranges implementing `RangeSize` support the `size` function.
--/
-instance [RangeSize su α] [UpwardEnumerable α] [SupportsUpperBound su α] :
-    IteratorSize (RangeIterator su α) Id where
-  size it := match it.internalState.next with
-    | none => pure (.up 0)
-    | some next => pure (.up (RangeSize.size it.internalState.upperBound next))
-
-/--
-Returns the number of elements contained in the given range, given that ranges of the given
-type and shape support this function.
--/
-@[always_inline, inline]
-def size {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
-    [SupportsUpperBound su α] (r : PRange ⟨sl, su⟩ α)
-    [IteratorSize (RangeIterator su α) Id] : Nat :=
-  PRange.Internal.iter r |>.size
-
-section Iterator
-
-theorem RangeIterator.isPlausibleIndirectOutput_iff {su α}
-    [UpwardEnumerable α] [SupportsUpperBound su α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α]
-    {it : Iter (α := RangeIterator su α) α} {out : α} :
-    it.IsPlausibleIndirectOutput out ↔
-      ∃ n, it.internalState.next.bind (UpwardEnumerable.succMany? n ·) = some out ∧
-        SupportsUpperBound.IsSatisfied it.internalState.upperBound out := by
-  constructor
-  · intro h
-    induction h
-    case direct h =>
-      rw [RangeIterator.isPlausibleOutput_iff] at h
-      refine ⟨0, by simp [h, LawfulUpwardEnumerable.succMany?_zero]⟩
-    case indirect h _ ih =>
-      rw [RangeIterator.isPlausibleSuccessorOf_iff] at h
-      obtain ⟨n, hn⟩ := ih
-      obtain ⟨a, ha, h₁, h₂, h₃⟩ := h
-      refine ⟨n + 1, ?_⟩
-      simp [ha, ← h₃, hn.2, LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, h₂, hn]
-  · rintro ⟨n, hn, hu⟩
-    induction n generalizing it
-    case zero =>
-      apply Iter.IsPlausibleIndirectOutput.direct
-      rw [RangeIterator.isPlausibleOutput_iff]
-      exact ⟨by simpa [LawfulUpwardEnumerable.succMany?_zero] using hn, hu⟩
-    case succ ih =>
-      cases hn' : it.internalState.next
-      · simp [hn'] at hn
-      rename_i a
-      simp only [hn', Option.bind_some] at hn
-      have hle : UpwardEnumerable.LE a out := ⟨_, hn⟩
-      rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn
-      cases hn' : UpwardEnumerable.succ? a
-      · simp only [hn', Option.bind_none, reduceCtorEq] at hn
-      rename_i a'
-      simp only [hn', Option.bind_some] at hn
-      specialize ih (it := ⟨some a', it.internalState.upperBound⟩) hn hu
-      refine Iter.IsPlausibleIndirectOutput.indirect ?_ ih
-      rw [RangeIterator.isPlausibleSuccessorOf_iff]
-      refine ⟨a, ‹_›, ?_, hn', rfl⟩
-      apply LawfulUpwardEnumerableUpperBound.isSatisfied_of_le _ a out
-      · exact hu
-      · exact hle
-
-theorem Internal.isPlausibleIndirectOutput_iter_iff {sl su α}
-    [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
-    [SupportsLowerBound sl α] [SupportsUpperBound su α]
-    [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLowerBound sl α]
-    {r : PRange ⟨sl, su⟩ α} {a : α} :
-    (PRange.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r := by
-  rw [RangeIterator.isPlausibleIndirectOutput_iff]
-  constructor
-  · rintro ⟨n, hn, hu⟩
-    refine ⟨?_, hu⟩
-    rw [LawfulUpwardEnumerableLowerBound.isSatisfied_iff]
-    cases hr : (PRange.Internal.iter r).internalState.next
-    · simp [hr] at hn
-    · rw [hr, Option.bind_some] at hn
-      exact ⟨_, hr, n, hn⟩
-  · rintro ⟨hl, hu⟩
-    rw [LawfulUpwardEnumerableLowerBound.isSatisfied_iff] at hl
-    obtain ⟨_, hr, n, hn⟩ := hl
-    exact ⟨n, by simp [PRange.Internal.iter, hr, hn], hu⟩
-
-theorem RangeIterator.upwardEnumerableLe_of_isPlausibleIndirectOutput {su α}
-    [UpwardEnumerable α] [SupportsUpperBound su α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α]
-    {it : Iter (α := RangeIterator su α) α} {out : α}
-    (hout : it.IsPlausibleIndirectOutput out) :
-    ∃ a, it.internalState.next = some a ∧ UpwardEnumerable.LE a out := by
-  have ⟨a, ha⟩ := Option.isSome_iff_exists.mp <|
-    RangeIterator.isSome_next_of_isPlausibleIndirectOutput hout
-  refine ⟨a, ha, ?_⟩
-  simp only [isPlausibleIndirectOutput_iff, ha, Option.bind_some, exists_and_right] at hout
-  exact hout.1
-
-@[no_expose]
-instance {sl su α m} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
-    [SupportsLowerBound sl α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
-    [Monad m] [Finite (RangeIterator su α) Id] :
-    ForIn' m (PRange ⟨sl, su⟩ α) α inferInstance where
-  forIn' r init f := by
-    haveI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
-    haveI := Iter.instForIn' (α := RangeIterator su α) (β := α) (n := m)
-    refine ForIn'.forIn' (α := α) (PRange.Internal.iter r) init (fun a ha acc => f a ?_ acc)
-    simp only [Membership.mem] at ha
-    rwa [PRange.Internal.isPlausibleIndirectOutput_iter_iff] at ha
-
-end Iterator
-
-end Std.PRange

src/Init/Data/Range/Polymorphic/Lemmas.lean

@@ -8,9 +8,9 @@ module
 prelude
 import Init.Data.Iterators
 import Init.Data.Iterators.Lemmas.Consumers.Collect
-import all Init.Data.Range.Polymorphic.Basic
+import all Init.Data.Range.Polymorphic.PRange
 import all Init.Data.Range.Polymorphic.RangeIterator
-import all Init.Data.Range.Polymorphic.Iterators
+import all Init.Data.Range.Polymorphic.Basic
 import all Init.Data.Iterators.Consumers.Loop
 
 /-!
@@ -274,29 +274,6 @@ private theorem Internal.forIn'_eq_forIn'_iter [UpwardEnumerable α]
       ForIn'.forIn' (Internal.iter r) init (fun a ha acc => f a (Internal.isPlausibleIndirectOutput_iter_iff.mp ha) acc) := by
   rfl
 
-theorem forIn'_eq_forIn'_toList [UpwardEnumerable α]
-    [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
-    [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
-    {r : PRange ⟨sl, su⟩ α}
-    {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
-    {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} :
-    ForIn'.forIn' r init f =
-      ForIn'.forIn' r.toList init (fun a ha acc => f a (mem_toList_iff_mem.mp ha) acc) := by
-  simp [Internal.forIn'_eq_forIn'_iter, Internal.toList_eq_toList_iter,
-    Iter.forIn'_eq_forIn'_toList]
-
-theorem forIn'_toList_eq_forIn' [UpwardEnumerable α]
-    [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
-    [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
-    {r : PRange ⟨sl, su⟩ α}
-    {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
-    {f : (a : α) → _ → γ → m (ForInStep γ)} :
-    ForIn'.forIn' r.toList init f =
-      ForIn'.forIn' r init (fun a ha acc => f a (mem_toList_iff_mem.mpr ha) acc) := by
-  simp [forIn'_eq_forIn'_toList]
-
 theorem mem_of_mem_open [UpwardEnumerable α]
     [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
     [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
@@ -323,39 +300,6 @@ theorem SupportsLowerBound.isSatisfied_init? {sl} [UpwardEnumerable α]
   simp only [LawfulUpwardEnumerableLowerBound.isSatisfied_iff]
   exact ⟨a, h, UpwardEnumerable.le_refl _⟩
 
-theorem forIn'_eq_match {sl su} [UpwardEnumerable α]
-    [SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
-    [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
-    [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
-    [SupportsLowerBound .open α] [LawfulUpwardEnumerableLowerBound .open α]
-    {r : PRange ⟨sl, su⟩ α}
-    {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
-    {f : (a : α) → _ → γ → m (ForInStep γ)} :
-    ForIn'.forIn' r init f = match hi : BoundedUpwardEnumerable.init? r.lower with
-      | none => pure init
-      | some a => if hu : SupportsUpperBound.IsSatisfied r.upper a then do
-        match ← f a ⟨SupportsLowerBound.isSatisfied_init? hi, hu⟩ init with
-        | .yield c =>
-          ForIn'.forIn' (α := α) (β := γ) (PRange.mk (shape := ⟨.open, su⟩) a r.upper) c
-            (fun a ha acc => f a (mem_of_mem_open (SupportsLowerBound.isSatisfied_init? hi) ha) acc)
-        | .done c => return c
-      else
-        return init := by
-  rw [Internal.forIn'_eq_forIn'_iter, Iter.forIn'_eq_match_step]
-  simp only [RangeIterator.step_eq_step, RangeIterator.step, Internal.iter]
-  apply Eq.symm
-  split <;> rename_i heq
-  · simp [heq]
-  · simp only [heq]
-    split
-    · simp only
-      apply bind_congr
-      intro step
-      split
-      · simp [Internal.forIn'_eq_forIn'_iter, Internal.iter, BoundedUpwardEnumerable.init?]
-      · simp
-    · simp
-
 instance {su} [UpwardEnumerable α] [SupportsUpperBound su α] [RangeSize su α]
     [LawfulUpwardEnumerable α] [HasFiniteRanges su α] [LawfulRangeSize su α] :
     LawfulIteratorSize (RangeIterator su α) where

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -108,16 +108,6 @@ theorem RangeIterator.step_eq_step {su} [UpwardEnumerable α] [SupportsUpperBoun
     it.step = ⟨RangeIterator.step it, isPlausibleStep_iff.mpr rfl⟩ := by
   simp [Iter.step, step_eq_monadicStep, Monadic.step_eq_step, IterM.Step.toPure]
 
-@[always_inline, inline]
-instance RepeatIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α]
-    {n : Type u → Type w} [Monad n] :
-    IteratorLoop (RangeIterator su α) Id n :=
-  .defaultImplementation
-
-instance RepeatIterator.instIteratorLoopPartial {su} [UpwardEnumerable α] [SupportsUpperBound su α]
-    {n : Type u → Type w} [Monad n] : IteratorLoopPartial (RangeIterator su α) Id n :=
-  .defaultImplementation
-
 instance RepeatIterator.instIteratorCollect {su} [UpwardEnumerable α] [SupportsUpperBound su α]
     {n : Type u → Type w} [Monad n] : IteratorCollect (RangeIterator su α) Id n :=
   .defaultImplementation
@@ -347,4 +337,109 @@ instance RangeIterator.instLawfulDeterministicIterator {su} [UpwardEnumerable α
     LawfulDeterministicIterator (RangeIterator su α) Id where
   isPlausibleStep_eq_eq it := ⟨Monadic.step it, rfl⟩
 
-end Std.PRange
+theorem RangeIterator.Monadic.isPlausibleIndirectOutput_iff {su α}
+    [UpwardEnumerable α] [SupportsUpperBound su α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α]
+    {it : IterM (α := RangeIterator su α) Id α} {out : α} :
+    it.IsPlausibleIndirectOutput out ↔
+      ∃ n, it.internalState.next.bind (UpwardEnumerable.succMany? n ·) = some out ∧
+        SupportsUpperBound.IsSatisfied it.internalState.upperBound out := by
+  constructor
+  · intro h
+    induction h
+    case direct h =>
+      rw [RangeIterator.Monadic.isPlausibleOutput_iff] at h
+      refine ⟨0, by simp [h, LawfulUpwardEnumerable.succMany?_zero]⟩
+    case indirect h _ ih =>
+      rw [RangeIterator.Monadic.isPlausibleSuccessorOf_iff] at h
+      obtain ⟨n, hn⟩ := ih
+      obtain ⟨a, ha, h₁, h₂, h₃⟩ := h
+      refine ⟨n + 1, ?_⟩
+      simp [ha, ← h₃, hn.2, LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, h₂, hn]
+  · rintro ⟨n, hn, hu⟩
+    induction n generalizing it
+    case zero =>
+      apply IterM.IsPlausibleIndirectOutput.direct
+      rw [RangeIterator.Monadic.isPlausibleOutput_iff]
+      exact ⟨by simpa [LawfulUpwardEnumerable.succMany?_zero] using hn, hu⟩
+    case succ ih =>
+      cases hn' : it.internalState.next
+      · simp [hn'] at hn
+      rename_i a
+      simp only [hn', Option.bind_some] at hn
+      have hle : UpwardEnumerable.LE a out := ⟨_, hn⟩
+      rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn
+      cases hn' : UpwardEnumerable.succ? a
+      · simp only [hn', Option.bind_none, reduceCtorEq] at hn
+      rename_i a'
+      simp only [hn', Option.bind_some] at hn
+      specialize ih (it := ⟨some a', it.internalState.upperBound⟩) hn hu
+      refine IterM.IsPlausibleIndirectOutput.indirect ?_ ih
+      rw [RangeIterator.Monadic.isPlausibleSuccessorOf_iff]
+      refine ⟨a, ‹_›, ?_, hn', rfl⟩
+      apply LawfulUpwardEnumerableUpperBound.isSatisfied_of_le _ a out
+      · exact hu
+      · exact hle
+
+theorem RangeIterator.isPlausibleIndirectOutput_iff {su α}
+    [UpwardEnumerable α] [SupportsUpperBound su α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α]
+    {it : Iter (α := RangeIterator su α) α} {out : α} :
+    it.IsPlausibleIndirectOutput out ↔
+      ∃ n, it.internalState.next.bind (UpwardEnumerable.succMany? n ·) = some out ∧
+        SupportsUpperBound.IsSatisfied it.internalState.upperBound out := by
+  simp only [Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM,
+    Monadic.isPlausibleIndirectOutput_iff, Iter.toIterM]
+
+section IteratorLoop
+
+/-!
+## Efficient `IteratorLoop` instance
+As long as the compiler cannot optimize away the `Option` in the internal state, we use a special
+loop implementation.
+-/
+
+@[always_inline, inline]
+instance RangeIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α]
+    {n : Type u → Type w} [Monad n] :
+    IteratorLoop (RangeIterator su α) Id n where
+  forIn _ γ Pl wf it init f :=
+    match it with
+    | ⟨⟨some next, upperBound⟩⟩ =>
+      if hu : SupportsUpperBound.IsSatisfied upperBound next then
+        loop γ Pl wf upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
+      else
+        return init
+    | ⟨⟨none, _⟩⟩ => return init
+  where
+    @[specialize]
+    loop γ Pl wf (upperBound : Bound su α) least acc
+        (f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
+        (next : α) (hl : UpwardEnumerable.LE least next) (hu : SupportsUpperBound.IsSatisfied upperBound next) : n γ := do
+      match ← f next hl hu acc with
+      | ⟨.yield acc', h⟩ =>
+        match hs : UpwardEnumerable.succ? next with
+        | some next' =>
+          if hu : SupportsUpperBound.IsSatisfied upperBound next' then
+            loop γ Pl wf upperBound least acc' f next' ?hle' hu
+          else
+            return acc'
+        | none => return acc'
+      | ⟨.done acc', _⟩ => return acc'
+    termination_by IteratorLoop.WFRel.mk wf ⟨⟨some next, upperBound⟩⟩ acc
+    decreasing_by
+      simp [IteratorLoop.rel, RangeIterator.Monadic.isPlausibleStep_iff,
+        RangeIterator.Monadic.step, IteratorLoop.WFRel.mk, *]
+  finally
+    case hf =>
+      rw [RangeIterator.Monadic.isPlausibleIndirectOutput_iff]
+      obtain ⟨n, hn⟩ := ha₁
+      exact ⟨n, hn, ha₂⟩
+    case hle =>
+      exact UpwardEnumerable.le_refl _
+    case hle' =>
+      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
+      simp [UpwardEnumerable.succMany?_one, hs]
+
+end Std.PRange.IteratorLoop

src/Init/Data/Slice.lean

@@ -9,8 +9,7 @@ prelude
 import Init.Data.Slice.Basic
 import Init.Data.Slice.Notation
 import Init.Data.Slice.Operations
-import Init.Data.Slice.Array.Basic
-import Init.Data.Slice.Array.Iterator
+import Init.Data.Slice.Array
 
 /-!
 # Polymorphic slices

src/Init/Data/Slice/Array.lean

@@ -7,12 +7,11 @@ module
 
 prelude
 import Init.Core
-import Init.Data.Slice.Array.Basic
+import Init.Data.Array.Subarray
 import Init.Data.Iterators.Combinators.Attach
 import Init.Data.Iterators.Combinators.FilterMap
 import all Init.Data.Range.Polymorphic.Basic
 import Init.Data.Range.Polymorphic.Nat
-import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Slice.Operations
 
 /-!
@@ -24,6 +23,12 @@ open Std Slice PRange Iterators
 
 variable {shape : RangeShape} {α : Type u}
 
+instance [ClosedOpenIntersection shape Nat] :
+    Sliceable shape (Array α) Nat (Subarray α) where
+  mkSlice xs range :=
+    let halfOpenRange := ClosedOpenIntersection.intersection range (0)...<xs.size
+    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)
+
 instance {s : Subarray α} : ToIterator s Id α :=
   .of _
     (PRange.Internal.iter (s.internalRepresentation.start...<s.internalRepresentation.stop)

src/Init/Data/Slice/Array/Basic.lean

@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-import Init.Core
-import Init.Data.Array.Subarray
-import Init.Data.Slice.Notation
-import Init.Data.Range.Polymorphic.Nat
-
-/-!
-This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator
-for those slices.
--/
-
-open Std Slice PRange
-
-variable {shape : RangeShape} {α : Type u}
-
-instance [ClosedOpenIntersection shape Nat] :
-    Sliceable shape (Array α) Nat (Subarray α) where
-  mkSlice xs range :=
-    let halfOpenRange := ClosedOpenIntersection.intersection range 0...<xs.size
-    (xs.toSubarray halfOpenRange.lower halfOpenRange.upper)

src/Init/Data/Stream.lean

@@ -6,9 +6,8 @@ Authors: Sebastian Ullrich, Andrew Kent, Leonardo de Moura
 module
 
 prelude
-import Init.Data.Range
 import Init.Data.Array.Subarray
-private import Init.Data.Slice.Array.Basic
+import Init.Data.Range
 
 /-!
 Remark: we considered using the following alternative design
@@ -67,9 +66,8 @@ instance (priority := low) [Stream ρ α] : ForIn m ρ α where
 instance : ToStream (List α) (List α) where
   toStream c := c
 
-@[no_expose]
 instance : ToStream (Array α) (Subarray α) where
-  toStream a := a[*...*]
+  toStream a := a[:a.size]
 
 instance : ToStream (Subarray α) (Subarray α) where
   toStream a := a

src/Init/Data/Vector/Basic.lean

@@ -13,7 +13,6 @@ import Init.Data.Array.MapIdx
 import Init.Data.Array.InsertIdx
 import Init.Data.Array.Range
 import Init.Data.Range
-private import Init.Data.Slice.Array.Basic
 import Init.Data.Stream
 
 /-!
@@ -543,9 +542,8 @@ instance : ForM m (Vector α n) α where
 
 /-! ### ToStream instance -/
 
-@[no_expose]
 instance : ToStream (Vector α n) (Subarray α) where
-  toStream xs := xs.toArray[*...*]
+  toStream xs := xs.toArray[:n]
 
 /-! ### Lexicographic ordering -/
 

src/Init/NotationExtra.lean

@@ -13,6 +13,7 @@ import Init.Conv
 import Init.Meta
 import Init.While
 meta import Init.Data.Option.Basic
+meta import Init.Data.Array.Subarray
 
 namespace Lean
 
@@ -286,8 +287,8 @@ macro_rules
         `(List.cons $x $k)
     else
       let m := x.size / 2
-      let y := x.drop m
-      let z := x.take m
+      let y := x[m:]
+      let z := x[:m]
       `(let y := %[ $[$y],* | $k ]
         %[ $[$z],* | y ])
 

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -393,7 +393,7 @@ def updateFunDeclParamsAssignment (params : Array Param) (args : Array Arg) : In
   to top.
   -/
   if params.size != args.size then
-    for param in params[args.size...*] do
+    for param in params[args.size:] do
       ret := (← findVarValue param.fvarId) == .bot
       updateVarAssignment param.fvarId .top
   return ret
@@ -475,7 +475,7 @@ where
           return .top
       | none =>
         let some (.ctorInfo info) := env.find? declName | return .top
-        let args := args[info.numParams...*].toArray
+        let args := args[info.numParams:].toArray
         if info.numFields == args.size then
           return .ctor declName (← args.mapM findArgValue)
         else

src/Lean/Compiler/LCNF/InferType.lean

@@ -180,7 +180,7 @@ mutual
         if structVal.numParams + structVal.numIndices != structTypeArgs.size then
           failed ()
         else do
-          let mut ctorType ← inferAppType (mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[*...structVal.numParams])
+          let mut ctorType ← inferAppType (mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[:structVal.numParams])
           for _ in [:idx] do
             match ctorType with
             | .forallE _ _ body _ =>
@@ -292,7 +292,7 @@ def mkCasesResultType (alts : Array Alt) : CompilerM Expr := do
   if alts.isEmpty then
     throwError "`Code.bind` failed, empty `cases` found"
   let mut resultType ← alts[0]!.inferType
-  for alt in alts[1...*] do
+  for alt in alts[1:] do
     resultType := joinTypes resultType (← alt.inferType)
   return resultType
 

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -20,7 +20,7 @@ def getRelevantCtorFields (ctorName : Name) : CoreM (Array Bool) := do
   Meta.MetaM.run' do
     Meta.forallTelescopeReducing info.type fun xs _ => do
       let mut result := #[]
-      for x in xs[info.numParams...*] do
+      for x in xs[info.numParams:] do
         let type ← Meta.inferType x
         result := result.push !(← Meta.isProp type <||> Meta.isTypeFormerType type)
       return result
@@ -104,7 +104,7 @@ where
     | .const declName us =>
       if let some info ← hasTrivialStructure? declName then
         let ctorType ← getOtherDeclBaseType info.ctorName []
-        toMonoType (getParamTypes (← instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
+        toMonoType (getParamTypes (← instantiateForall ctorType args[:info.numParams]))[info.fieldIdx]!
       else
         let mut result := mkConst declName
         let mut type ← getOtherDeclBaseType declName us

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -19,7 +19,7 @@ abbrev M := ReaderT LocalContext CompilerM
 private def join (as : Array α) (f : α → M Format) : M Format := do
   if h : 0 < as.size then
     let mut result ← f as[0]
-    for a in as[1...*] do
+    for a in as[1:] do
       result := f!"{result} {← f a}"
     return result
   else

src/Lean/Compiler/LCNF/Probing.lean

@@ -165,10 +165,10 @@ def count : Probe α Nat := fun data => return #[data.size]
 def sum : Probe Nat Nat := fun data => return #[data.foldl (init := 0) (·+·)]
 
 @[inline]
-def tail (n : Nat) : Probe α α := fun data => return data[(data.size - n)...*]
+def tail (n : Nat) : Probe α α := fun data => return data[data.size - n:]
 
 @[inline]
-def head (n : Nat) : Probe α α := fun data => return data[*...n]
+def head (n : Nat) : Probe α α := fun data => return data[:n]
 
 def runOnDeclsNamed (declNames : Array Name) (probe : Probe Decl β) (phase : Phase := Phase.base): CoreM (Array β) := do
   let ext := getExt phase

src/Lean/Compiler/LCNF/ReduceArity.lean

@@ -83,10 +83,10 @@ def visitLetValue (e : LetValue) : FindUsedM Unit := do
             visitFVar fvarId
         | .erased | .type .. => pure ()
       -- over-application
-      for arg in args[decl.params.size...*] do
+      for arg in args[decl.params.size:] do
         visitArg arg
       -- partial-application
-      for param in decl.params[args.size...*] do
+      for param in decl.params[args.size:] do
         -- If recursive function is partially applied, we assume missing parameters are used because we don't want to eta-expand.
         visitFVar param.fvarId
     else

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

@@ -74,7 +74,7 @@ def getIndInfo? (type : Expr) : CoreM (Option (List Level × Array Arg)) := do
   let .const declName us := type.getAppFn | return none
   let .inductInfo info ← getConstInfo declName | return none
   unless type.getAppNumArgs >= info.numParams do return none
-  let args := type.getAppArgs[*...info.numParams].toArray.map fun
+  let args := type.getAppArgs[:info.numParams].toArray.map fun
     | .fvar fvarId => .fvar fvarId
     | e => if e.isErased then .erased else .type e
   return some (us, args)

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -137,9 +137,9 @@ where
 /-- Create the arguments for a jump to an auxiliary join point created using `mkJpAlt`. -/
 private def mkJmpNewArgs (args : Array Arg) (targetParamIdx : Nat) (fields : Array Arg) (dependsOnTarget : Bool) : Array Arg :=
   if dependsOnTarget then
-    args[*...=targetParamIdx] ++ fields ++ args[targetParamIdx<...*]
+    args[:targetParamIdx+1] ++ fields ++ args[targetParamIdx+1:]
   else
-    args[*...targetParamIdx] ++ fields ++ args[targetParamIdx<...*]
+    args[:targetParamIdx] ++ fields ++ args[targetParamIdx+1:]
 
 /--
 Create the arguments for a jump to an auxiliary join point created using `mkJpAlt`.
@@ -283,7 +283,7 @@ where
     else
       match ctorInfo with
       | .ctor ctorVal ctorArgs =>
-         let fields := ctorArgs[ctorVal.numParams...*]
+         let fields := ctorArgs[ctorVal.numParams:]
          let argsNew := mkJmpNewArgs args info.paramIdx fields jpAlt.dependsOnDiscr
          return some <| .jmp jpAlt.decl.fvarId argsNew
       | .natVal 0 =>

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -48,7 +48,7 @@ def specializePartialApp (info : InlineCandidateInfo) : SimpM FunDecl := do
   for param in info.params, arg in info.args do
     subst := subst.insert param.fvarId arg
   let mut paramsNew := #[]
-  for param in info.params[info.args.size...*] do
+  for param in info.params[info.args.size:] do
     let type ← replaceExprFVars param.type subst (translator := true)
     let paramNew ← mkAuxParam type
     paramsNew := paramsNew.push paramNew
@@ -130,7 +130,7 @@ partial def inlineApp? (letDecl : LetDecl) (k : Code) : SimpM (Option Code) := d
     markSimplified
     simp (.fun funDecl k)
   else
-    let code ← betaReduce info.params info.value info.args[*...info.arity]
+    let code ← betaReduce info.params info.value info.args[:info.arity]
     if k.isReturnOf fvarId && numArgs == info.arity then
       /- Easy case, the continuation `k` is just returning the result of the application. -/
       markSimplified
@@ -140,7 +140,7 @@ partial def inlineApp? (letDecl : LetDecl) (k : Code) : SimpM (Option Code) := d
       let simpK (result : FVarId) : SimpM Code := do
         /- `result` contains the result of the inlined code -/
         if numArgs > info.arity then
-          let decl ← mkAuxLetDecl (.fvar result info.args[info.arity...*])
+          let decl ← mkAuxLetDecl (.fvar result info.args[info.arity:])
           addFVarSubst fvarId decl.fvarId
           simp (.let decl k)
         else
@@ -157,7 +157,7 @@ partial def inlineApp? (letDecl : LetDecl) (k : Code) : SimpM (Option Code) := d
       --  return none
       else
         markSimplified
-        let expectedType ← inferAppType info.fType info.args[*...info.arity]
+        let expectedType ← inferAppType info.fType info.args[:info.arity]
         if expectedType.headBeta.isForall then
           /-
           If `code` returns a function, we create an auxiliary local function declaration (and eta-expand it)
@@ -199,7 +199,7 @@ partial def simpCasesOnCtor? (cases : Cases) : SimpM (Option Code) := do
     | .alt _ params k =>
       match ctorInfo with
       | .ctor ctorVal ctorArgs =>
-        let fields := ctorArgs[ctorVal.numParams...*]
+        let fields := ctorArgs[ctorVal.numParams:]
         for param in params, field in fields do
           addSubst param.fvarId field
         let k ← simp k

src/Lean/Compiler/LCNF/Specialize.lean

@@ -243,7 +243,7 @@ where
         -- Keep the parameter
         let param := { param with type := param.type.instantiateLevelParamsNoCache decl.levelParams us }
         params := params.push (← internalizeParam param)
-    for param in decl.params[argMask.size...*] do
+    for param in decl.params[argMask.size:] do
       let param := { param with type := param.type.instantiateLevelParamsNoCache decl.levelParams us }
       params := params.push (← internalizeParam param)
     let code := code.instantiateValueLevelParams decl.levelParams us
@@ -266,7 +266,7 @@ def getRemainingArgs (paramsInfo : Array SpecParamInfo) (args : Array Arg) : Arr
   for info in paramsInfo, arg in args do
     if info matches .other then
       result := result.push arg
-  return result ++ args[paramsInfo.size...*]
+  return result ++ args[paramsInfo.size:]
 
 def paramsToGroundVars (params : Array Param) : CompilerM FVarIdSet :=
   params.foldlM (init := {}) fun r p => do

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -27,9 +27,9 @@ private def normalizeAlt (e : Expr) (numParams : Nat) : MetaM Expr :=
     if xs.size == numParams then
       return e
     else if xs.size > numParams then
-      let body ← Meta.mkLambdaFVars xs[numParams...*] body
+      let body ← Meta.mkLambdaFVars xs[numParams:] body
       let body ← Meta.withLetDecl (← mkFreshUserName `_k) (← Meta.inferType body) body fun x => Meta.mkLetFVars #[x] x
-      Meta.mkLambdaFVars xs[*...numParams] body
+      Meta.mkLambdaFVars xs[:numParams] body
     else
       Meta.forallBoundedTelescope (← Meta.inferType e) (numParams - xs.size) fun ys _ =>
         Meta.mkLambdaFVars (xs ++ ys) (mkAppN e ys)

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -117,7 +117,7 @@ where
                   let mut subst := {}
                   let mut jpArgs := #[]
                   /- Remark: `funDecl.params.size` may be greater than `args.size`. -/
-                  for param in funDecl.params[*...args.size] do
+                  for param in funDecl.params[:args.size] do
                     let type ← replaceExprFVars param.type subst (translator := true)
                     let paramNew ← mkAuxParam type
                     jpParams := jpParams.push paramNew
@@ -165,7 +165,7 @@ where
       | .unreach _ =>
         let type ← c.inferType
         eraseCode c
-        seq[*...i].forM fun
+        seq[:i].forM fun
           | .let decl => eraseLetDecl decl
           | .jp decl | .fun decl => eraseFunDecl decl
           | .cases _ cs => eraseCode (.cases cs)
@@ -500,7 +500,7 @@ where
   Otherwise return
   ```
   let k := app
-  k args[arity...*]
+  k args[arity:]
   ```
   -/
   mkOverApplication (app : Arg) (args : Array Expr) (arity : Nat) : M Arg := do
@@ -550,7 +550,7 @@ where
   visitCases (casesInfo : CasesInfo) (e : Expr) : M Arg :=
     etaIfUnderApplied e casesInfo.arity do
       let args := e.getAppArgs
-      let mut resultType ← toLCNFType (← liftMetaM do Meta.inferType (mkAppN e.getAppFn args[*...casesInfo.arity]))
+      let mut resultType ← toLCNFType (← liftMetaM do Meta.inferType (mkAppN e.getAppFn args[:casesInfo.arity]))
       if casesInfo.numAlts == 0 then
         /- `casesOn` of an empty type. -/
         mkUnreachable resultType
@@ -626,7 +626,7 @@ where
       let hb := mkLcProof args[1]!
       let minor := args[minorPos]!
       let minor := minor.beta #[ha, hb]
-      visit (mkAppN minor args[arity...*])
+      visit (mkAppN minor args[arity:])
 
   visitNoConfusion (e : Expr) : M Arg := do
     let .const declName _ := e.getAppFn | unreachable!
@@ -645,7 +645,7 @@ where
           etaIfUnderApplied e (arity+1) do
             let major := args[arity]!
             let major ← expandNoConfusionMajor major lhsCtorVal.numFields
-            let major := mkAppN major args[(arity+1)...*]
+            let major := mkAppN major args[arity+1:]
             visit major
         else
           let type ← toLCNFType (← liftMetaM <| Meta.inferType e)

src/Lean/Compiler/LCNF/ToMono.lean

@@ -54,12 +54,12 @@ def argToMonoDeferredCheck (resultFVar : FVarId) (arg : Arg) : ToMonoM Arg :=
 
 def ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array Arg)
     : ToMonoM LetValue := do
-  let argsNewParams : Array Arg ← args[*...ctorInfo.numParams].toArray.mapM fun arg => do
+  let argsNewParams : Array Arg ← args[:ctorInfo.numParams].toArray.mapM fun arg => do
     -- We only preserve constructor parameters that are types
     match arg with
     | .type type => return .type (← toMonoType type)
     | .fvar .. | .erased => return .erased
-  let argsNewFields ← args[ctorInfo.numParams...*].toArray.mapM (argToMonoDeferredCheck resultFVar)
+  let argsNewFields ← args[ctorInfo.numParams:].toArray.mapM (argToMonoDeferredCheck resultFVar)
   let argsNew := argsNewParams ++ argsNewFields
   return .const ctorInfo.name [] argsNew
 

src/Lean/Data/FuzzyMatching.lean

@@ -97,7 +97,7 @@ algorithm uses different scores for the last operation (miss/match). This is
 necessary to give consecutive character matches a bonus. -/
 private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Array CharRole) : Option Int := Id.run do
   /- Flattened array where the value at index (i, j, k) represents the best possible score of a fuzzy match
-  between the substrings pattern[*...=i] and word[*...j] assuming that pattern[i] misses at word[j] (k = 0, i.e.
+  between the substrings pattern[:i+1] and word[:j+1] assuming that pattern[i] misses at word[j] (k = 0, i.e.
   it was matched earlier), or matches at word[j] (k = 1). A value of `none` corresponds to a score of -∞, and is used
   where no such match/miss is possible or for unneeded parts of the table. -/
   let mut result : Array (Option Int) := Array.replicate (pattern.length * word.length * 2) none

src/Lean/Elab/App.lean

@@ -1173,7 +1173,7 @@ where
          If the motive is explicit (like for `False.rec`), then a positional `_` counts as "not provided". -/
       let mut args := args.toList
       let mut namedArgs := namedArgs.toList
-      for x in xs[*...elimInfo.motivePos] do
+      for x in xs[0:elimInfo.motivePos] do
         let localDecl ← x.fvarId!.getDecl
         match findBinderName? namedArgs localDecl.userName with
         | some _ => namedArgs := eraseNamedArg namedArgs localDecl.userName
@@ -1242,7 +1242,7 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N
   -- of the name resolving in the `structName` namespace.
   find? structName <||> do
     let resolutionOrder ← if isStructure env structName then getStructureResolutionOrder structName else pure #[structName]
-    for ns in resolutionOrder[1...resolutionOrder.size] do
+    for ns in resolutionOrder[1:resolutionOrder.size] do
       if let some res ← find? ns then
         return res
     return none

src/Lean/Elab/BuiltinNotation.lean

@@ -67,9 +67,9 @@ open Meta
             else if numExplicitFields == 0 then
               throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' does not have explicit fields, but #{args.size} provided"
             else
-              let extra := args[(numExplicitFields-1)...args.size]
+              let extra := args[numExplicitFields-1:args.size]
               let newLast ← `(⟨$[$extra],*⟩)
-              let newArgs := args[*...(numExplicitFields-1)].toArray.push newLast
+              let newArgs := args[0:numExplicitFields-1].toArray.push newLast
               `($(mkCIdentFrom stx ctor (canonical := true)) $(newArgs)*)
             withMacroExpansion stx newStx $ elabTerm newStx expectedType?
           | _ => throwError "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}")

src/Lean/Elab/ComputedFields.lean

@@ -51,7 +51,7 @@ with
   | .cons x l => x + l.sum
   @[computed_field] length : NatList → Nat
   | .nil => 0
-  | .cons _ l => l.length + 1
+  | .cons _ l => l.length + 1 
 ```
 -/
 @[builtin_doc]
@@ -116,8 +116,8 @@ def overrideCasesOn : M Unit := do
   mkCasesOn (name ++ `_impl)
   let value ←
     forallTelescope (← instantiateForall casesOn.type params) fun xs constMotive => do
-      let (indices, major, minors) := (xs[1...=numIndices].toArray,
-        xs[numIndices+1]!, xs[(numIndices+2)...*].toArray)
+      let (indices, major, minors) := (xs[1:numIndices+1].toArray,
+        xs[numIndices+1]!, xs[numIndices+2:].toArray)
       let majorImplTy := mkAppN (mkConst (name ++ `_impl) lparams) (params ++ indices)
       mkLambdaFVars (params ++ xs) <|
         mkAppN (mkConst (mkCasesOnName (name ++ `_impl))
@@ -201,8 +201,8 @@ def mkComputedFieldOverrides (declName : Name) (compFields : Array Name) : MetaM
   let lparams := ind.levelParams.map mkLevelParam
   forallTelescope ind.type fun paramsIndices _ => do
   withLocalDeclD `x (mkAppN (mkConst ind.name lparams) paramsIndices) fun val => do
-    let params := paramsIndices[*...ind.numParams].toArray
-    let indices := paramsIndices[ind.numParams...*].toArray
+    let params := paramsIndices[:ind.numParams].toArray
+    let indices := paramsIndices[ind.numParams:].toArray
     let compFieldVars := compFields.map fun fieldDeclName =>
       (fieldDeclName.updatePrefix .anonymous,
         fun _ => do inferType (← mkAppM fieldDeclName (params ++ indices ++ #[val])))

src/Lean/Elab/Declaration.lean

@@ -196,7 +196,7 @@ private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array S
       else if i == 0 then
         none -- `mutual` block does not contain any preamble commands
       else
-        some (elems[*...i], elems[i...elems.size])
+        some (elems[0:i], elems[i:elems.size])
     else
       none -- a `mutual` block containing only preamble commands is not a valid `mutual` block
   loop 0

src/Lean/Elab/DefView.lean

@@ -140,20 +140,20 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[2]
   let modifiers       := modifiers.addAttr { name := `inline }
   let modifiers       := modifiers.addAttr { name := `reducible }
-  { ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.abbrev, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3] }
 
 def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
   let (binders, type) := expandOptDeclSig stx[2]
   let deriving? := if stx[4].isNone then none else some stx[4][1].getSepArgs
-  { ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.def, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.def, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3], deriving? }
 
 def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "theorem " >> declId >> declSig >> declVal
   let (binders, type) := expandDeclSig stx[2]
-  { ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.theorem, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.theorem, modifiers,
     declId := stx[1], binders, type? := some type, value := stx[3] }
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
@@ -174,7 +174,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
       trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}"
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx[1] id (canonical := true), mkNullNode]
   return {
-    ref := stx, headerRef := mkNullNode stx.getArgs[*...5], kind := DefKind.instance, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.instance, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[5]
   }
 
@@ -187,7 +187,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
       let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%)
       `(Parser.Command.declValSimple| := $val)
   return {
-    ref := stx, headerRef := mkNullNode stx.getArgs[*...3], kind := DefKind.opaque, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.opaque, modifiers := modifiers,
     declId := stx[1], binders := binders, type? := some type, value := val
   }
 
@@ -196,7 +196,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[1]
   let id              := mkIdentFrom stx[0] `_example (canonical := true)
   let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
-  { ref := stx, headerRef := mkNullNode stx.getArgs[*...2], kind := DefKind.example, modifiers := modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:2], kind := DefKind.example, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[2] }
 
 def isDefLike (stx : Syntax) : Bool :=

src/Lean/Elab/Deriving/BEq.lean

@@ -67,7 +67,7 @@ where
                 rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs)
             /- If `x` appears in the type of another field, use `eq_of_beq` to
                unify the types of the subsequent variables -/
-            else if ← xs[(pos+1)...*].anyM
+            else if ← xs[pos+1:].anyM
                 (fun fvar => (Expr.containsFVar · x.fvarId!) <$> (inferType fvar)) then
               rhs ← `(if h : $a:ident == $b:ident then by
                         cases (eq_of_beq h)

src/Lean/Elab/Deriving/Inhabited.lean

@@ -83,7 +83,7 @@ where
   mkInstanceCmd? : TermElabM (Option Syntax) := do
     let ctorVal ← getConstInfoCtor ctorName
     forallTelescopeReducing ctorVal.type fun xs _ =>
-      addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do
+      addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
         let mut usedInstIdxs := {}
         let mut ok := true
         for h : i in [ctorVal.numParams:xs.size] do

src/Lean/Elab/Deriving/ToExpr.lean

@@ -123,9 +123,9 @@ def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) (le
   for indVal in ctx.typeInfos, auxFunName in ctx.auxFunNames do
     let currArgNames ← mkInductArgNames indVal
     let numParams    := indVal.numParams
-    let currIndices  := currArgNames[numParams...*]
+    let currIndices  := currArgNames[numParams:]
     let binders      ← mkImplicitBinders currIndices
-    let argNamesNew  := argNames[*...numParams] ++ currIndices
+    let argNamesNew  := argNames[:numParams] ++ currIndices
     let indType      ← mkInductiveApp indVal argNamesNew
     let instName     ← mkFreshUserName `localinst
     let toTypeExpr   ← mkToTypeExpr indVal argNames

src/Lean/Elab/Deriving/Util.lean

@@ -91,9 +91,9 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array
     let auxFunName   := ctx.auxFunNames[i]!
     let currArgNames ← mkInductArgNames indVal
     let numParams    := indVal.numParams
-    let currIndices  := currArgNames[numParams...*]
+    let currIndices  := currArgNames[numParams:]
     let binders      ← mkImplicitBinders currIndices
-    let argNamesNew  := argNames[*...numParams] ++ currIndices
+    let argNamesNew  := argNames[:numParams] ++ currIndices
     let indType      ← mkInductiveApp indVal argNamesNew
     let type         ← `($(mkCIdent className) $indType)
     let val          ← `(⟨$(mkIdent auxFunName)⟩)
@@ -154,7 +154,7 @@ def mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElab
 def mkDiscrs (header : Header) (indVal : InductiveVal) : TermElabM (Array (TSyntax ``Parser.Term.matchDiscr)) := do
   let mut discrs := #[]
   -- add indices
-  for argName in header.argNames[indVal.numParams...*] do
+  for argName in header.argNames[indVal.numParams:] do
     discrs := discrs.push (← mkDiscr argName)
   return discrs ++ (← header.targetNames.mapM mkDiscr)
 

src/Lean/Elab/ErrorExplanation.lean

@@ -76,7 +76,7 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do
   -- term and so leave `stx` unchanged. The in-progress identifier will always be the penultimate
   -- argument of `span`.
   let span := if stx.getNumArgs == numArgsExpected then
-    stx.setArgs (stx.getArgs[*...(stx.getNumArgs - 1)])
+    stx.setArgs (stx.getArgs[0:stx.getNumArgs - 1])
   else
     stx
   let partialId := span[span.getNumArgs - 2]

src/Lean/Elab/Inductive.lean

@@ -156,7 +156,7 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
        -/
       let C := type.getAppFn
       let binderNames := getArrowBinderNames (← instantiateMVars (← inferType C))
-      return replaceArrowBinderNames r binderNames[*...bsPrefix.size]
+      return replaceArrowBinderNames r binderNames[:bsPrefix.size]
 
 /--
   Elaborate constructor types.

src/Lean/Elab/Level.lean

@@ -60,11 +60,11 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
     elabLevel (stx.getArg 1)
   else if kind == ``Lean.Parser.Level.max then
     let args := stx.getArg 1 |>.getArgs
-    args[*...(args.size - 1)].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
       return mkLevelMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.imax then
     let args := stx.getArg 1 |>.getArgs
-    args[*...(args.size - 1)].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
+    args[:args.size - 1].foldrM (init := ← elabLevel args.back!) fun stx lvl =>
       return mkLevelIMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.hole then
     mkFreshLevelMVar

src/Lean/Elab/Match.lean

@@ -334,7 +334,7 @@ private partial def eraseIndices (type : Expr) : MetaM Expr := do
   let type' ← whnfD type
   matchConstInduct type'.getAppFn (fun _ => return type) fun info _ => do
     let args := type'.getAppArgs
-    let params ← args[*...info.numParams].toArray.mapM eraseIndices
+    let params ← args[:info.numParams].toArray.mapM eraseIndices
     let result := mkAppN type'.getAppFn params
     let resultType ← inferType result
     let (newIndices, _, _) ← forallMetaTelescopeReducing resultType (some (args.size - info.numParams))

src/Lean/Elab/MutualInductive.lean

@@ -389,7 +389,7 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType)
           for i in [numParams:arity] do
             unless i < xs.size && xs[i]! == typeArgs[i]! do -- Remark: if we want to allow arguments to be rearranged, this test should be xs.contains typeArgs[i]
               maskRef.modify fun mask => mask.set! i false
-          for x in xs[numParams...*] do
+          for x in xs[numParams:] do
             let xType ← inferType x
             let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar)
             xType.forEachWhere (stopWhenVisited := true) cond fun e => do
@@ -448,7 +448,7 @@ private def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveTy
   -- the order of indices generated by the auto implicit feature.
   let mask := masks[0]!
   forallBoundedTelescope indTypes[0]!.type numParams fun params type => do
-    let otherTypes ← indTypes[1...*].toArray.mapM fun indType => do whnfD (← instantiateForall indType.type params)
+    let otherTypes ← indTypes[1:].toArray.mapM fun indType => do whnfD (← instantiateForall indType.type params)
     let ctorTypes ← indTypes.toList.mapM fun indType => indType.ctors.mapM fun ctor => do whnfD (← instantiateForall ctor.type params)
     let typesToCheck := otherTypes.toList ++ ctorTypes.flatten
     let rec go (i : Nat) (type : Expr) (typesToCheck : List Expr) : MetaM Nat := do
@@ -618,7 +618,7 @@ where
     indTypes.forM fun indType => indType.ctors.forM fun ctor =>
       withCtorRef views ctor.name do
         forallTelescopeReducing ctor.type fun ctorParams _ =>
-          for ctorParam in ctorParams[numParams...*] do
+          for ctorParam in ctorParams[numParams:] do
             accLevelAtCtor ctorParam r rOffset
 
 /--
@@ -710,7 +710,7 @@ private partial def propagateUniversesToConstructors (numParams : Nat) (indTypes
     let k := u.getOffset
     indTypes.forM fun indType => indType.ctors.forM fun ctor =>
       forallTelescopeReducing ctor.type fun ctorArgs _ => do
-        for ctorArg in ctorArgs[numParams...*] do
+        for ctorArg in ctorArgs[numParams:] do
           let type ← inferType ctorArg
           let v := (← instantiateLevelMVars (← getLevel type)).normalize
           if v.hasMVar then
@@ -768,7 +768,7 @@ private def checkResultingUniverses (views : Array InductiveView) (elabs' : Arra
       elabs'[i]!.checkUniverses numParams u
       indType.ctors.forM fun ctor =>
       forallTelescopeReducing ctor.type fun ctorArgs _ => do
-        for ctorArg in ctorArgs[numParams...*] do
+        for ctorArg in ctorArgs[numParams:] do
           let type ← inferType ctorArg
           let v := (← instantiateLevelMVars (← getLevel type)).normalize
           unless u.geq v do

src/Lean/Elab/PatternVar.lean

@@ -275,7 +275,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     let arg0 ← collect args[0]!
     let stateNew ← get
     let mut argsNew := #[arg0]
-    for arg in args[1...*] do
+    for arg in args[1:] do
       set stateSaved
       argsNew := argsNew.push (← collect arg)
       unless samePatternsVariables stateSaved.vars.size stateNew (← get) do

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -221,7 +221,7 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
     root.forEach fun e => do
       if let some info := isMatcherAppCore? env e then
         let args := e.getAppArgs
-        for discr in args[info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs)] do
+        for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
           if (← Meta.isConstructorApp discr) then
             throwThe Unit ()
   return (← (find e).run) matches .error _

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -422,12 +422,12 @@ where
         if _ : j < varyingArgs.size then
           go (i + 1) (j + 1) (xs.push varyingArgs[j])
         else
-          if perm[i...*].all Option.isNone then
+          if perm[i:].all Option.isNone then
             xs -- Under-application
           else
             panic! "FixedParams.buildArgs: too few varying args"
     else
-      xs ++ varyingArgs[j...*] -- (Possibly) over-application
+      xs ++ varyingArgs[j:] -- (Possibly) over-application
 
 /--
 Are all fixed parameters a non-reordered prefix?

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -71,8 +71,8 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
     unless numIndParams + numTypeFormers < args.size do
       trace[Elab.definition.structural] "unexpected 'below' type{indentExpr belowType}"
       throwToBelowFailed
-    let params := args[*...numIndParams]
-    let finalArgs := args[(numIndParams+numTypeFormers)...*]
+    let params := args[:numIndParams]
+    let finalArgs := args[numIndParams+numTypeFormers:]
     let pre := mkAppN f params
     let motiveTypes ← inferArgumentTypesN numTypeFormers pre
     let numMotives : Nat := positions.numIndices

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -71,8 +71,8 @@ def getRecArgInfo (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array
     let xType ← whnfD localDecl.type
     matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
     let indArgs    : Array Expr := xType.getAppArgs
-    let indParams  : Array Expr := indArgs[*...indInfo.numParams]
-    let indIndices : Array Expr := indArgs[indInfo.numParams...*]
+    let indParams  : Array Expr := indArgs[0:indInfo.numParams]
+    let indIndices : Array Expr := indArgs[indInfo.numParams:]
     if !indIndices.all Expr.isFVar then
       throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
     else if !indIndices.allDiff then

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -100,7 +100,7 @@ def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) :=
   assert! recInfo.numMotives = igi.numMotives
   let aux := mkAppN (.const recName (0 :: igi.levels)) igi.params
   let motives ← inferArgumentTypesN recInfo.numMotives aux
-  let auxMotives : Array Expr := motives[igi.all.size...*]
+  let auxMotives : Array Expr := motives[igi.all.size:]
   auxMotives.mapM fun motive =>
     forallTelescopeReducing motive fun xs _ => do
       assert! xs.size > 0

src/Lean/Elab/PreDefinition/Structural/IndPred.lean

@@ -29,7 +29,7 @@ private def replaceIndPredRecApp (fixedParamPerm : FixedParamPerm) (funType : Ex
           trace[Elab.definition.structural] "too few arguments, expected {t.getAppNumArgs}, found {ys.size}. Underapplied recursive call?"
           return false
         if (← (t.getAppArgs.zip ys).allM (fun (t,s) => isDefEq t s)) then
-          main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) ys[t.getAppNumArgs...*])
+          main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) ys[t.getAppNumArgs:])
           return ← mvars.allM fun v => do
             unless (← v.mvarId!.isAssigned) do
               trace[Elab.definition.structural] "Cannot use {mkFVar localDecl.fvarId}: parameter {v} remains unassigned"

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -50,7 +50,7 @@ where
       let r := mkApp F (← loop F args[fixedPrefixSize]!)
       let decreasingProp := (← whnf (← inferType r)).bindingDomain!
       let r := mkApp r (← mkDecreasingProof decreasingProp)
-      return mkAppN r (← args[fixedPrefixSize<...*].toArray.mapM (loop F))
+      return mkAppN r (← args[fixedPrefixSize+1:].toArray.mapM (loop F))
 
   processApp (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     if e.isAppOf recFnName then
@@ -150,7 +150,7 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v
     let minor ← lambdaTelescope args[4]! fun xs body => do
         let a := xs[0]!
         let xNew := xs[1]!
-        let valNew ← mkLambdaFVars xs[2...*] body
+        let valNew ← mkLambdaFVars xs[2:] body
         let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM `PSigma.mk #[α, β, a, xNew])
         withLocalDeclD FDecl.userName FTypeNew fun FNew => do
           mkLambdaFVars #[a, xNew, FNew] (← processPSigmaCasesOn xNew FNew valNew k)

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -348,7 +348,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedParamPerms : FixedParamP
   lambdaBoundedTelescope unaryPreDef.value (fixedParamPerms.numFixed + 1) fun xs body => do
     unless xs.size == fixedParamPerms.numFixed + 1 do
       throwError "Unexpected number of lambdas in unary pre-definition"
-    let ys := xs[*...fixedParamPerms.numFixed]
+    let ys := xs[:fixedParamPerms.numFixed]
     let param := xs[fixedParamPerms.numFixed]!
     withRecApps unaryPreDef.declName fixedParamPerms.numFixed param body fun param args => do
       unless args.size ≥ fixedParamPerms.numFixed + 1 do
@@ -755,7 +755,7 @@ def mkProdElem (xs : Array Expr) : MetaM Expr := do
   | 1 => return xs[0]!
   | _ =>
     let n := xs.size
-    xs[*...(n-1)].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
+    xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
 
 def toTerminationMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
     (userVarNamess : Array (Array Name)) (measuress : Array (Array BasicMeasure))

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -26,8 +26,8 @@ open Meta
 def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr := do
   let args := e.getAppArgs
   if n ≤ args.size then
-    let e' ← k args[*...n]
-    return mkAppN e' args[n...*]
+    let e' ← k args[:n]
+    return mkAppN e' args[n:]
   else
     let missing := n - args.size
     forallBoundedTelescope (← inferType e) missing fun xs _ => do

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -195,7 +195,7 @@ def preprocess (e : Expr) : MetaM Simp.Result := do
       e.withApp fun f as => do
         if f.isConstOf ``wfParam then
           if h : as.size ≥ 2 then
-            return .continue (mkAppN as[1] as[2...*])
+            return .continue (mkAppN as[1] as[2:])
         return .continue
 
     -- Transform `have`s to `let`s for non-propositions.

src/Lean/Elab/Print.lean

@@ -125,7 +125,7 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
       let flatCtorName := mkFlatCtorOfStructCtorName ctor
       let flatCtorInfo ← getConstInfo flatCtorName
       let autoParams : NameMap Syntax ← forallTelescope flatCtorInfo.type fun args _ =>
-        args[numParams...*].foldlM (init := {}) fun set arg => do
+        args[numParams:].foldlM (init := {}) fun set arg => do
           let decl ← arg.fvarId!.getDecl
           if let some (.const tacticDecl _) := decl.type.getAutoParamTactic? then
             let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl

src/Lean/Elab/Quotation.lean

@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[*...(ids.size - 1)].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
+              let arr ← ids[:ids.size - 1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
               `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))

src/Lean/Elab/SetOption.lean

@@ -14,7 +14,7 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
   -- We include the first argument (the keyword) for position information in case `id` is `missing`.
-  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
+  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[0:3]))
   let optionName := id.getId.eraseMacroScopes
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
   pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }

src/Lean/Elab/StructInst.lean

@@ -246,7 +246,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sourcesView : SourcesView) (ex
     let valFirst  := rest[0]
     let valFirst  := if valFirst.getKind == ``Lean.Parser.Term.structInstArrayRef then valFirst else valFirst[1]
     let restArgs  := rest.getArgs
-    let valRest   := mkNullNode restArgs[1...restArgs.size]
+    let valRest   := mkNullNode restArgs[1:restArgs.size]
     let valField  := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
     let valSource := mkSourcesWithSyntax #[s]
     let val       := stx.setArg 1 valSource
@@ -662,7 +662,7 @@ private def reduceFieldProjs (e : Expr) : StructInstM Expr := do
           if let some major := args[projInfo.numParams]? then
             if major.isAppOfArity projInfo.ctorName (cval.numParams + cval.numFields) then
               if let some arg := major.getAppArgs[projInfo.numParams + projInfo.i]? then
-                return TransformStep.visit <| mkAppN arg args[projInfo.numParams<...*]
+                return TransformStep.visit <| mkAppN arg args[projInfo.numParams+1:]
     return TransformStep.continue
   Meta.transform e (post := postVisit)
 

src/Lean/Elab/Structure.lean

@@ -506,7 +506,7 @@ private def reduceFieldProjs (e : Expr) (zetaDelta := true) : StructElabM Expr :
                 pure major
             if major.isAppOfArity projInfo.ctorName (cval.numParams + cval.numFields) then
               if let some arg := major.getAppArgs[projInfo.numParams + projInfo.i]? then
-                return TransformStep.visit <| mkAppN arg args[(projInfo.numParams+1)...*]
+                return TransformStep.visit <| mkAppN arg args[projInfo.numParams+1:]
     return TransformStep.continue
   Meta.transform e (post := postVisit)
 
@@ -1412,7 +1412,7 @@ private def addParentInstances (parents : Array StructureParentInfo) : MetaM Uni
   -- A parent is an ancestor of the others if it appears with index ≥ 1 in one of the resolution orders.
   let resOrders : Array (Array Name) ← instParents.mapM fun parent => getStructureResolutionOrder parent.structName
   let instParents := instParents.filter fun parent =>
-    !resOrders.any (fun resOrder => resOrder[1...*].any (· == parent.structName))
+    !resOrders.any (fun resOrder => resOrder[1:].any (· == parent.structName))
   for instParent in instParents do
     addInstance instParent.projFn AttributeKind.global (eval_prio default)
 

src/Lean/Elab/Syntax.lean

@@ -25,7 +25,7 @@ private def mkParserSeq (ds : Array (Term × Nat)) : TermElabM (Term × Nat) :=
     pure ds[0]
   else
     let mut (r, stackSum) := ds[0]
-    for (d, stackSz) in ds[1...ds.size] do
+    for (d, stackSz) in ds[1:ds.size] do
       r ← `(ParserDescr.binary `andthen $r $d)
       stackSum := stackSum + stackSz
     return (r, stackSum)

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -373,7 +373,7 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
     error := error ++ "3. The original goal was reduced to False and is thus invalid."
     throwError error
   else
-    let sat := sats[1...*].foldl (init := sats[0]) SatAtBVLogical.and
+    let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and
     return {
       bvExpr := ShareCommon.shareCommon sat.bvExpr,
       proveFalse := sat.proveFalse,

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -62,7 +62,7 @@ where
         let oldParsed := old.val.get
         oldInner? := oldParsed.inner? |>.map (⟨oldParsed.stx, ·⟩)
     -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script
-    Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1...*])) fun stxs => do
+    Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do
       let some snap := (← readThe Term.Context).tacSnap?
         | do evalTactic tac; goOdd stxs
       let mut reusableResult? := none
@@ -118,7 +118,7 @@ where
       return
     saveTacticInfoForToken stx[0] -- add `TacticInfo` node for `;`
     -- disable further reuse on separator change as to not reuse wrong `TacticInfo`
-    Term.withNarrowedTacticReuse (fun stx => (stx[0], mkNullNode stx.getArgs[1...*])) goEven stx
+    Term.withNarrowedTacticReuse (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) goEven stx
 
 @[builtin_tactic seq1] def evalSeq1 : Tactic := fun stx =>
   evalSepTactics stx[0]

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -66,8 +66,8 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) (
     if congrThm.argKinds.size == 0 then
       throwError "'congr' conv tactic failed to create congruence theorem"
     let (proof', mvarIdsNew', mvarIdsNewInsts') ←
-      mkCongrThm origTag eNew args[funInfo.getArity...*] addImplicitArgs nameSubgoals
-    for arg in args[funInfo.getArity...*] do
+      mkCongrThm origTag eNew args[funInfo.getArity:] addImplicitArgs nameSubgoals
+    for arg in args[funInfo.getArity:] do
       proof ← Meta.mkCongrFun proof arg
     proof ← mkEqTrans proof proof'
     mvarIdsNew := mvarIdsNew ++ mvarIdsNew'
@@ -144,7 +144,7 @@ private partial def mkCongrArgZeroThm (tacticName : String) (origTag : Name) (f
       proof := mkApp proof rhs
       mvarIdsNewInsts := mvarIdsNewInsts.push rhs.mvarId!
     | .heq | .fixedNoParam => unreachable!
-  let proof' ← args[congrThm.argKinds.size...*].foldlM (init := proof) mkCongrFun
+  let proof' ← args[congrThm.argKinds.size:].foldlM (init := proof) mkCongrFun
   return (proof', mvarIdNew?.get!, mvarIdsNewInsts)
 
 /--
@@ -202,7 +202,7 @@ where
       if i < 0 || i ≥ xs.size then
         throwError "invalid '{tacticName}' tactic, application has {xs.size} argument(s) but the index is out of bounds"
       let idx := i.natAbs
-      return (mkAppN f xs[*...idx], xs[idx...*])
+      return (mkAppN f xs[0:idx], xs[idx:])
     else
       let mut fType ← inferType f
       let mut j := 0
@@ -219,7 +219,7 @@ where
       if i < 0 || i ≥ explicitIdxs.size then
         throwError "invalid '{tacticName}' tactic, application has {explicitIdxs.size} explicit argument(s) but the index is out of bounds"
       let idx := explicitIdxs[i.natAbs]!
-      return (mkAppN f xs[*...idx], xs[idx...*])
+      return (mkAppN f xs[0:idx], xs[idx:])
 
 def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit := do
   if i == 0 then

src/Lean/Elab/Tactic/Ext.lean

@@ -78,7 +78,7 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
     unless xIdx + 1 == yIdx do
       throwError "expecting {x} and {y} to be consecutive arguments"
     let startIdx := yIdx + 1
-    let toRevert := args[startIdx...*].toArray
+    let toRevert := args[startIdx:].toArray
     let fvars ← toRevert.foldlM (init := {}) (fun st e => return collectFVars st (← inferType e))
     for fvar in toRevert do
       unless ← Meta.isProof fvar do
@@ -88,11 +88,11 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
     let conj := mkAndN (← toRevert.mapM (inferType ·)).toList
     -- Make everything implicit except for inst implicits
     let mut newBis := #[]
-    for fvar in args[*...startIdx] do
+    for fvar in args[0:startIdx] do
       if (← fvar.fvarId!.getBinderInfo) matches .default | .strictImplicit then
         newBis := newBis.push (fvar.fvarId!, .implicit)
     withNewBinderInfos newBis do
-      mkForallFVars args[*...startIdx] <| mkIff ty conj
+      mkForallFVars args[:startIdx] <| mkIff ty conj
 
 /--
 Ensures that the given structure has an ext theorem, without validating any pre-existing theorems.
@@ -308,8 +308,8 @@ def extCore (g : MVarId) (pats : List (TSyntax `rcasesPat))
     let (used, gs) ← extCore (← getMainGoal) pats.toList depth
     if RCases.linter.unusedRCasesPattern.get (← getOptions) then
       if used < pats.size then
-        Linter.logLint RCases.linter.unusedRCasesPattern (mkNullNode pats[used...*].toArray)
-          m!"`ext` did not consume the patterns: {pats[used...*]}"
+        Linter.logLint RCases.linter.unusedRCasesPattern (mkNullNode pats[used:].toArray)
+          m!"`ext` did not consume the patterns: {pats[used:]}"
     replaceMainGoal <| gs.map (·.1) |>.toList
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/Induction.lean

@@ -207,14 +207,14 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
       throwError "Internal error in mkElimApp: Expected application of {motive}:{indentExpr s.fType}"
     -- Sanity-checking that the motive is applied to the targets.
     -- NB: The motive can take them in a different order than the eliminator itself
-    for motiveArg in motiveArgs[*...targets.size] do
+    for motiveArg in motiveArgs[:targets.size] do
       unless targets.contains motiveArg do
         throwError "Internal error in mkElimApp: Expected first {targets.size} arguments of motive \
           in conclusion to be one of the targets:{indentExpr s.fType}"
-    pure motiveArgs[targets.size...*]
+    pure motiveArgs[targets.size:]
   let elimApp ← instantiateMVars s.f
   -- `elimArgs` is the argument list that the offsets in `elimInfo` work with
-  let elimArgs := elimApp.getAppArgs[elimInfo.elimExpr.getAppNumArgs...*]
+  let elimArgs := elimApp.getAppArgs[elimInfo.elimExpr.getAppNumArgs:]
   return { elimApp, elimArgs, alts, others, motive, complexArgs }
 
 /--
@@ -586,7 +586,7 @@ private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
       let altStxs := optInductionAlts[0].getArg 2
       let inner := if altStxs.getNumArgs > 0 then altStxs else optInductionAlts[0][0]
       -- `with` and tactic applied to all branches must be unchanged for reuse
-      (mkNullNode optInductionAlts[0].getArgs[*...2], inner))
+      (mkNullNode optInductionAlts[0].getArgs[:2], inner))
     (fun alts? =>
       if optInductionAlts.isNone then      -- no `with` clause
         cont none
@@ -832,10 +832,10 @@ def elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ide
             j := j + 1
           else
             result := result.push info.expr
-        -- note: `fvarIdsNew[j...*]` contains all the `h` variables
+        -- note: `fvarIdsNew[j:]` contains all the `h` variables
         let hIdents := infos.filterMap (·.view.hIdent?)
         assert! hIdents.size + j == fvarIdsNew.size
-        return ((result, hIdents.zip fvarIdsNew[j...*]), [mvarId])
+        return ((result, hIdents.zip fvarIdsNew[j:]), [mvarId])
 
 /--
 Generalize targets in `fun_induction` and `fun_cases`. Should behave like `elabCasesTargets` with

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -70,9 +70,9 @@ def mkEvalRflProof (e : Expr) (lc : LinearCombo) : OmegaM Expr := do
 def mkCoordinateEvalAtomsEq (e : Expr) (n : Nat) : OmegaM Expr := do
   if n < 10 then
     let atoms ← atoms
-    let tail ← mkListLit (.const ``Int []) atoms[n<...*].toArray.toList
+    let tail ← mkListLit (.const ``Int []) atoms[n+1:].toArray.toList
     let lem := .str ``LinearCombo s!"coordinate_eval_{n}"
-    mkEqSymm (mkAppN (.const lem []) (atoms[*...=n].toArray.push tail))
+    mkEqSymm (mkAppN (.const lem []) (atoms[:n+1].toArray.push tail))
   else
     let atoms ← atomsCoeffs
     let n := toExpr n

src/Lean/Elab/Tactic/RCases.lean

@@ -436,7 +436,7 @@ def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
     else
       result := result.push (mkFVar fvarIdsNew[j]!)
       j := j+1
-  pure (result, fvarIdsNew[j...*], goal)
+  pure (result, fvarIdsNew[j:], goal)
 
 /--
 Given a list of targets of the form `e` or `h : e`, and a pattern, match all the targets
@@ -524,7 +524,7 @@ partial def rintroContinue (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
     (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) : TermElabM α := do
   g.withContext (loop 0 g fs clears a)
 where
-  /-- Runs `rintroContinue` on `pats[i...*]` -/
+  /-- Runs `rintroContinue` on `pats[i:]` -/
   loop i g fs clears a := do
     if h : i < pats.size then
       rintroCore g fs clears a ref pats[i] ty? (loop (i+1))

src/Lean/Elab/Tactic/Try.lean

@@ -168,7 +168,7 @@ private def getTacsSolvedAll (tacs2 : Array (Array (TSyntax `tactic))) : Array (
   else
     let mut r := #[]
     for tac2 in tacs2[0]! do
-      if tacs2[1...*].all (·.contains tac2) then
+      if tacs2[1:].all (·.contains tac2) then
         r := r.push tac2
     return r
 
@@ -184,7 +184,7 @@ private def getKindsSolvedAll (tacss : Array (Array (TSyntax `tactic))) : Array
     let mut r := #[]
     for tacs0 in tacss[0]! do
       let k := tacs0.raw.getKind
-      if tacss[1...*].all fun tacs => tacs.any fun tac => tac.raw.getKind == k then
+      if tacss[1:].all fun tacs => tacs.any fun tac => tac.raw.getKind == k then
         r := r.push k
     return r
 
@@ -582,7 +582,7 @@ def evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) (config : Try.Config :=
     evalSuggest tac |>.run { terminal := true, root := tac, config }
   catch _ =>
     throwEvalAndSuggestFailed config
-  let s := (getSuggestions tac')[*...config.max].toArray
+  let s := (getSuggestions tac')[:config.max].toArray
   if s.isEmpty then
     throwEvalAndSuggestFailed config
   else

src/Lean/Elab/Term.lean

@@ -461,7 +461,7 @@ depend on them (i.e. they should not be inspected beforehand).
 def withNarrowedArgTacticReuse [Monad m] [MonadReaderOf Context m] [MonadLiftT BaseIO m]
     [MonadWithReaderOf Core.Context m] [MonadWithReaderOf Context m] [MonadOptions m]
     (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
-  withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[*...argIdx], stx[argIdx])) act stx
+  withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
 
 /--
 Disables incremental tactic reuse *and* reporting for `act` if `cond` is true by setting `tacSnap?`

src/Lean/Environment.lean

@@ -1810,7 +1810,7 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array
   let mut states := states
   let extDescrs ← persistentEnvExtensionsRef.get
   /- For extensions starting at `startingAt`, ensure their `importedEntries` array have size `mods.size`. -/
-  for extDescr in extDescrs[startingAt...*] do
+  for extDescr in extDescrs[startingAt:] do
     -- safety: as in `modifyState`
     states := unsafe extDescr.toEnvExtension.modifyStateImpl states fun s =>
       { s with importedEntries := .replicate mods.size #[] }

src/Lean/Meta/CollectMVars.lean

@@ -24,7 +24,7 @@ partial def collectMVars (e : Expr) : StateRefT CollectMVars.State MetaM Unit :=
   let resultSavedSize := s.result.size
   let s := e.collectMVars s
   set s
-  for mvarId in s.result[resultSavedSize...*] do
+  for mvarId in s.result[resultSavedSize:] do
     match (← getDelayedMVarAssignment? mvarId) with
     | none   => pure ()
     | some d => collectMVars (mkMVar d.mvarIdPending)

src/Lean/Meta/CongrTheorems.lean

@@ -301,13 +301,13 @@ where
                 go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq)
             | .fixed => go (i+1) (rhss.push lhss[i]!) (eqs.push none) hyps
             | .cast =>
-              let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[*...rhss.size]) rhss
+              let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
               let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs
               go (i+1) (rhss.push rhs) (eqs.push none) hyps
             | .subsingletonInst =>
               -- The `lhs` does not need to instance implicit since it can be inferred from the LHS
               withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do
-                let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[*...rhss.size]) rhss
+                let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
                 let rhsBi   := if subsingletonInstImplicitRhs then .instImplicit else .implicit
                 withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs =>
                   go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs)

src/Lean/Meta/Constructions/BRecOn.lean

@@ -67,10 +67,10 @@ private def mkBelowFromRec (recName : Name) (nParams : Nat)
 
   let decl ← forallTelescope recVal.type fun refArgs _ => do
     assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
-    let params  : Array Expr := refArgs[*...nParams]
-    let motives : Array Expr := refArgs[nParams...(nParams + recVal.numMotives)]
-    let minors  : Array Expr := refArgs[(nParams + recVal.numMotives)...(nParams + recVal.numMotives + recVal.numMinors)]
-    let indices : Array Expr := refArgs[(nParams + recVal.numMotives + recVal.numMinors)...(refArgs.size - 1)]
+    let params  : Array Expr := refArgs[:nParams]
+    let motives : Array Expr := refArgs[nParams:nParams + recVal.numMotives]
+    let minors  : Array Expr := refArgs[nParams + recVal.numMotives:nParams + recVal.numMotives + recVal.numMinors]
+    let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
     let major   : Expr       := refArgs[refArgs.size - 1]!
 
     -- universe parameter of the type fomer.
@@ -194,10 +194,10 @@ private def mkBRecOnFromRec (recName : Name) (nParams : Nat)
 
   let decl ← forallTelescope recVal.type fun refArgs refBody => do
     assert! refArgs.size > nParams + recVal.numMotives + recVal.numMinors
-    let params  : Array Expr := refArgs[*...nParams]
-    let motives : Array Expr := refArgs[nParams...(nParams + recVal.numMotives)]
-    let minors  : Array Expr := refArgs[(nParams + recVal.numMotives)...(nParams + recVal.numMotives + recVal.numMinors)]
-    let indices : Array Expr := refArgs[(nParams + recVal.numMotives + recVal.numMinors)...(refArgs.size - 1)]
+    let params  : Array Expr := refArgs[:nParams]
+    let motives : Array Expr := refArgs[nParams:nParams + recVal.numMotives]
+    let minors  : Array Expr := refArgs[nParams + recVal.numMotives:nParams + recVal.numMotives + recVal.numMinors]
+    let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
     let major   : Expr       := refArgs[refArgs.size - 1]!
 
     let some idx := motives.idxOf? refBody.getAppFn

src/Lean/Meta/Constructions/NoConfusionLinear.lean

@@ -192,7 +192,7 @@ def mkNoConfusionTypeLinear (indName : Name) : MetaM Unit := do
                 let alt := mkApp alt PType
                 let alt := mkApp alt (mkRawNatLit i)
                 let k ← forallTelescopeReducing (← inferType alt).bindingDomain! fun zs2 _ => do
-                  let eqs ← (Array.zip zs1 zs2[1...*]).filterMapM fun (z1,z2) => do
+                  let eqs ← (Array.zip zs1 zs2[1:]).filterMapM fun (z1,z2) => do
                     if (← isProof z1) then
                       return none
                     else

src/Lean/Meta/Constructions/RecOn.lean

@@ -22,9 +22,9 @@ def mkRecOn (n : Name) : MetaM Unit := do
     -- fow:    As Cs indices major-premise minor-premises
     let AC_size := xs.size - recInfo.numMinors - recInfo.numIndices - 1
     let vs :=
-      xs[*...AC_size] ++
-      xs[(AC_size + recInfo.numMinors)...(AC_size + recInfo.numMinors + 1 + recInfo.numIndices)] ++
-      xs[(AC_size)...(AC_size + recInfo.numMinors)]
+      xs[:AC_size] ++
+      xs[AC_size + recInfo.numMinors:AC_size + recInfo.numMinors + 1 + recInfo.numIndices] ++
+      xs[AC_size:AC_size + recInfo.numMinors]
     let type ← mkForallFVars vs t
     let value ← mkLambdaFVars vs e
     mkDefinitionValInferrringUnsafe (mkRecOnName n) recInfo.levelParams type value .abbrev

src/Lean/Meta/DiscrTree.lean

@@ -535,7 +535,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
       else if let some matcherInfo := isMatcherAppCore? (← getEnv) e then
         -- A matcher application is stuck is one of the discriminants has a metavariable
         let args := e.getAppArgs
-        for arg in args[matcherInfo.getFirstDiscrPos...(matcherInfo.getFirstDiscrPos + matcherInfo.numDiscrs)] do
+        for arg in args[matcherInfo.getFirstDiscrPos: matcherInfo.getFirstDiscrPos + matcherInfo.numDiscrs] do
           if arg.hasExprMVar then
             Meta.throwIsDefEqStuck
       else if (← isRec c) then

src/Lean/Meta/ExprDefEq.lean

@@ -79,7 +79,7 @@ where
       else if (← isDefEq (← inferType a) (← inferType b)) then
         checkpointDefEq do
           let args := b.getAppArgs
-          let params := args[*...ctorVal.numParams].toArray
+          let params := args[:ctorVal.numParams].toArray
           for h : i in [ctorVal.numParams : args.size] do
             let j := i - ctorVal.numParams
             let proj ← mkProjFn ctorVal us params j a
@@ -1125,9 +1125,9 @@ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool :=
         checkTypesAndAssign mvar v
 
 /--
-  Auxiliary procedure for solving `?m args =?= v` when `args[*...patternVarPrefix]` contains
+  Auxiliary procedure for solving `?m args =?= v` when `args[:patternVarPrefix]` contains
   only pairwise distinct free variables.
-  Let `args[*...patternVarPrefix] = #[a₁, ..., aₙ]`, and `args[patternVarPrefix...*] = #[b₁, ..., bᵢ]`,
+  Let `args[:patternVarPrefix] = #[a₁, ..., aₙ]`, and `args[patternVarPrefix:] = #[b₁, ..., bᵢ]`,
   this procedure first reduces the constraint to
   ```
   ?m a₁ ... aₙ =?= fun x₁ ... xᵢ => v
@@ -1151,7 +1151,7 @@ private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patter
   else if patternVarPrefix == 0 then
     defaultCase
   else
-    let argsPrefix : Array Expr := args[*...patternVarPrefix]
+    let argsPrefix : Array Expr := args[:patternVarPrefix]
     let type ← instantiateForall mvarDecl.type argsPrefix
     let suffixSize := numArgs - argsPrefix.size
     forallBoundedTelescope type suffixSize fun xs _ => do
@@ -1195,7 +1195,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
         let args := args.set i arg
         match arg with
         | .fvar fvarId =>
-          if args[*...i].any fun prevArg => prevArg == arg then
+          if args[0:i].any fun prevArg => prevArg == arg then
             useFOApprox args
           else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then
             useFOApprox args

src/Lean/Meta/IndPredBelow.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dany Fabian
 -/
 prelude
+import Init.Data.Range.Polymorphic.Nat
 import Lean.Meta.Constructions.CasesOn
 import Lean.Meta.Match.Match
 import Lean.Meta.Tactic.SolveByElim
@@ -81,7 +82,7 @@ where
   addMotives (motives : Array (Name × Expr)) (numParams : Nat) : Expr → MetaM Expr :=
     motives.foldrM (fun (motiveName, motive) t =>
       forallTelescopeReducing t fun xs s => do
-        let motiveType ← instantiateForall motive xs[*...numParams]
+        let motiveType ← instantiateForall motive xs[:numParams]
         withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
           mkForallFVars (xs.insertIdxIfInBounds numParams motive) s)
 
@@ -100,9 +101,9 @@ partial def mkCtorType
     { innerType := t
       indVal := #[]
       motives := #[]
-      params := xs[*...ctx.numParams]
-      args := xs[ctx.numParams...*]
-      target := xs[*...ctx.numParams] }
+      params := xs[:ctx.numParams]
+      args := xs[ctx.numParams:]
+      target := xs[:ctx.numParams] }
 where
   addHeaderVars (vars : Variables) := do
     let headersWithNames ← ctx.headers.mapIdxM fun idx header =>
@@ -137,7 +138,7 @@ where
           (mkConst originalCtor.name $ ctx.typeInfos[0]!.levelParams.map mkLevelParam)
           (vars.params ++ vars.args)
       let innerType := mkAppN vars.indVal[belowIdx]! $
-        vars.params ++ vars.motives ++ args[ctx.numParams...*] ++ #[hApp]
+        vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
       let x ← mkForallFVars vars.target innerType
       return replaceTempVars vars x
 
@@ -178,7 +179,7 @@ where
             let hApp := mkAppN binder xs
             let t :=
               mkAppN vars.indVal[idx]! $
-                vars.params ++ vars.motives ++ args[ctx.numParams...*] ++ #[hApp]
+                vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
             let newDomain ← mkForallFVars xs t
 
             withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain (k idx)
@@ -195,7 +196,7 @@ where
       let t ← whnf t
       t.withApp fun _ args => do
         let hApp := mkAppN binder xs
-        let t := mkAppN vars.motives[indValIdx]! $ args[ctx.numParams...*] ++ #[hApp]
+        let t := mkAppN vars.motives[indValIdx]! $ args[ctx.numParams:] ++ #[hApp]
         let newDomain ← mkForallFVars xs t
 
         withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain k
@@ -331,9 +332,9 @@ def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
 where
   mkType : MetaM Expr :=
     forallTelescopeReducing ctx.headers[idx]! fun xs _ => do
-    let params := xs[*...ctx.numParams]
-    let motives := xs[ctx.numParams...(ctx.numParams + ctx.motives.size)].toArray
-    let indices := xs[(ctx.numParams + ctx.motives.size)...*]
+    let params := xs[:ctx.numParams]
+    let motives := xs[ctx.numParams:ctx.numParams + ctx.motives.size].toArray
+    let indices := xs[ctx.numParams + ctx.motives.size:]
     let motiveBinders ← ctx.motives.mapIdxM $ mkIH params motives
     withLocalDeclsD motiveBinders fun ys => do
     mkForallFVars (xs ++ ys) (mkAppN motives[idx]! indices)
@@ -387,7 +388,7 @@ private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Na
   (← whnf (← inferType xs[idx]!)).withApp fun type args => do
     let indName := type.constName!
     let indInfo ← getConstInfoInduct indName
-    let belowArgs := args[*...indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams...*] ++ #[xs[idx]!]
+    let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]!]
     let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs
     return (indName, belowType)
 
@@ -426,14 +427,14 @@ partial def mkBelowMatcher
     lambdaTelescope alt fun xs t => do
     let oldFVars := oldLhs.fvarDecls.toArray
     let fvars := lhs.fvarDecls.toArray.map (·.toExpr)
-    let xs : Array Expr :=
+    let xs :=
       -- special case: if we had no free vars, i.e. there was a unit added and no we do have free vars, we get rid of the unit.
       match oldFVars.size, fvars.size with
-      | 0, _+1 => xs[1...*].toArray
+      | 0, _+1 => xs[1:]
       | _, _ => xs
-    let t := t.replaceFVars xs[*...oldFVars.size] fvars[*...oldFVars.size]
-    trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[*...oldFVars.size] ++ xs[oldFVars.size...*] ++ fvars[oldFVars.size...*]}"
-    let newAlt ← mkLambdaFVars (fvars[*...oldFVars.size] ++ xs[oldFVars.size...*] ++ fvars[oldFVars.size...*]) t
+    let t := t.replaceFVars xs[:oldFVars.size] fvars[:oldFVars.size]
+    trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]}"
+    let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]) t
     trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}"
     pure newAlt
 
@@ -483,7 +484,7 @@ where
 
       let belowCtor ← getConstInfoCtor $ ctorName.updatePrefix $ ctorInfo.induct ++ `below
       let belowIndices ← IndPredBelow.getBelowIndices ctorName
-      let belowIndices := belowIndices[ctorInfo.numParams...*].toArray.map (· - belowCtor.numParams)
+      let belowIndices := belowIndices[ctorInfo.numParams:].toArray.map (· - belowCtor.numParams)
 
       -- belowFieldOpts starts off with an array of empty fields.
       -- We then go over pattern's fields and set the appropriate fields to values.
@@ -555,7 +556,7 @@ where
     lambdaTelescope matcherApp.motive fun xs t => do
     let numDiscrs := matcherApp.discrs.size
     withLocalDeclD (←mkFreshUserName `h_below) (belowType.replaceFVars ys xs) fun h_below => do
-    let motive ← mkLambdaFVars (xs[*...numDiscrs] ++ #[h_below] ++ xs[numDiscrs...*]) t
+    let motive ← mkLambdaFVars (xs[:numDiscrs] ++ #[h_below] ++ xs[numDiscrs:]) t
     trace[Meta.IndPredBelow.match] "motive := {motive}"
     return motive
 
@@ -601,6 +602,25 @@ def mkBelow (declName : Name) : MetaM Unit := do
     else trace[Meta.IndPredBelow] "Nested or not recursive"
   else trace[Meta.IndPredBelow] "Not inductive predicate"
 
+def mkBelow'' (declName : Name) : MetaM Unit := do
+  if (← isInductivePredicate declName) then
+    let x ← getConstInfoInduct declName
+    if x.isRec && !x.isNested then
+      let ctx ← IndPredBelow.mkContext declName
+      let decl ← IndPredBelow.mkBelowDecl ctx
+      addDecl decl
+      trace[Meta.IndPredBelow] "added {ctx.belowNames}"
+      ctx.belowNames.forM Lean.mkCasesOn
+      for i in *...ctx.typeInfos.size do
+        try
+          let decl ← IndPredBelow.mkBrecOnDecl ctx i
+          -- disable async TC so we can catch its exceptions
+          withOptions (Elab.async.set · false) do
+            addDecl decl
+        catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]!}\n{e.toMessageData}"
+    else trace[Meta.IndPredBelow] "Nested or not recursive"
+  else trace[Meta.IndPredBelow] "Not inductive predicate"
+
 builtin_initialize
   registerTraceClass `Meta.IndPredBelow
   registerTraceClass `Meta.IndPredBelow.match

src/Lean/Meta/InferType.lean

@@ -10,7 +10,7 @@ import Lean.Meta.Basic
 namespace Lean
 
 /--
-Auxiliary function for instantiating the loose bound variables in `e` with `args[start...stop]`.
+Auxiliary function for instantiating the loose bound variables in `e` with `args[start:stop]`.
 This function is similar to `instantiateRevRange`, but it applies beta-reduction when
 we instantiate a bound variable with a lambda expression.
 Example: Given the term `#0 a`, and `start := 0, stop := 1, args := #[fun x => x]` the result is
@@ -106,7 +106,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
     if structVal.numParams + structVal.numIndices != structTypeArgs.size then
       failed ()
     else do
-      let mut ctorType ← inferAppType (mkConst ctorVal.name structLvls) structTypeArgs[*...<structVal.numParams]
+      let mut ctorType ← inferAppType (mkConst ctorVal.name structLvls) structTypeArgs[:structVal.numParams]
       for i in [:idx] do
         ctorType ← whnf ctorType
         match ctorType with

src/Lean/Meta/Injective.lean

@@ -20,7 +20,7 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
     return none
   else
     let mut result := args.back!
-    for arg in args.reverse[1...*] do
+    for arg in args.reverse[1:] do
       result := mkApp2 (mkConst ``And) arg result
     return result
 

src/Lean/Meta/LazyDiscrTree.lean

@@ -206,7 +206,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) :
         -- A matcher application is stuck if one of the discriminants has a metavariable
         let args := e.getAppArgs
         let start := matcherInfo.getFirstDiscrPos
-        for arg in args[start...(start + matcherInfo.numDiscrs)] do
+        for arg in args[ start : start + matcherInfo.numDiscrs ] do
           if arg.hasExprMVar then
             Meta.throwIsDefEqStuck
       else if (← isRec c) then

src/Lean/Meta/LetToHave.lean

@@ -372,7 +372,7 @@ private partial def visitProj (e : Expr) (structName : Name) (idx : Nat) (struct
     let structTypeArgs := structType.getAppArgs
     if structVal.numParams + structVal.numIndices != structTypeArgs.size then
       failed ()
-    let mut ctorType ← inferType <| mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[*...structVal.numParams]
+    let mut ctorType ← inferType <| mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[:structVal.numParams]
     let mut args := #[]
     let mut j := 0
     let mut lastFieldTy : Expr := default

src/Lean/Meta/Match/MatchEqs.lean

@@ -518,7 +518,7 @@ where
     -- If we find one we must extend `convertCastEqRec`.
     unless e.isAppOf ``Eq.ndrec do return false
     unless e.getAppNumArgs > 6 do return false
-    for arg in e.getAppArgs[6...*] do
+    for arg in e.getAppArgs[6:] do
       if arg.isFVar && (← read).contains arg.fvarId! then
         return true
     return true
@@ -606,7 +606,7 @@ where
                 trace[Meta.Match.matchEqs] "altNew: {altNew} : {altTypeNew}"
                 -- Replace `rhs` with `x` (the lambda binder in the motive)
                 let mut altTypeNewAbst := (← kabstract altTypeNew rhs).instantiate1 x
-                -- Replace args[6...(6+i)] with `motiveTypeArgsNew`
+                -- Replace args[6:6+i] with `motiveTypeArgsNew`
                 for j in [:i] do
                   altTypeNewAbst := (← kabstract altTypeNewAbst argsNew[6+j]!).instantiate1 motiveTypeArgsNew[j]!
                 let localDecl ← motiveTypeArg.fvarId!.getDecl
@@ -623,7 +623,7 @@ where
       argsNew := argsNew.set! 2 motiveNew
       -- Construct the new minor premise for the `Eq.ndrec` application.
       -- First, we use `eqRecNewPrefix` to infer the new minor premise binders for `Eq.ndrec`
-      let eqRecNewPrefix := mkAppN f argsNew[*...3] -- `Eq.ndrec` minor premise is the fourth argument.
+      let eqRecNewPrefix := mkAppN f argsNew[:3] -- `Eq.ndrec` minor premise is the fourth argument.
       let .forallE _ minorTypeNew .. ← whnf (← inferType eqRecNewPrefix) | unreachable!
       trace[Meta.Match.matchEqs] "new minor type: {minorTypeNew}"
       let minor := args[3]!
@@ -750,11 +750,11 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
   let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos
   forallTelescopeReducing constInfo.type fun xs matchResultType => do
     let mut eqnNames := #[]
-    let params := xs[*...matchInfo.numParams]
+    let params := xs[:matchInfo.numParams]
     let motive := xs[matchInfo.getMotivePos]!
-    let alts   := xs[(xs.size - matchInfo.numAlts)...*]
+    let alts   := xs[xs.size - matchInfo.numAlts:]
     let firstDiscrIdx := matchInfo.numParams + 1
-    let discrs := xs[firstDiscrIdx...(firstDiscrIdx + matchInfo.numDiscrs)]
+    let discrs := xs[firstDiscrIdx : firstDiscrIdx + matchInfo.numDiscrs]
     let mut notAlts := #[]
     let mut idx := 1
     let mut splitterAltTypes := #[]
@@ -871,11 +871,11 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do
   let numDiscrEqs := matchInfo.getNumDiscrEqs
   forallTelescopeReducing constInfo.type fun xs _matchResultType => do
     let mut eqnNames := #[]
-    let params := xs[*...matchInfo.numParams]
+    let params := xs[:matchInfo.numParams]
     let motive := xs[matchInfo.getMotivePos]!
-    let alts   := xs[(xs.size - matchInfo.numAlts)...*]
+    let alts   := xs[xs.size - matchInfo.numAlts:]
     let firstDiscrIdx := matchInfo.numParams + 1
-    let discrs := xs[firstDiscrIdx...(firstDiscrIdx + matchInfo.numDiscrs)]
+    let discrs := xs[firstDiscrIdx : firstDiscrIdx + matchInfo.numDiscrs]
     let mut notAlts := #[]
     let mut idx := 1
     for i in [:alts.size] do

src/Lean/Meta/Match/MatcherApp/Basic.lean

@@ -40,10 +40,10 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
         discrInfos    := info.discrInfos
         params        := args.extract 0 info.numParams
         motive        := args[info.getMotivePos]!
-        discrs        := args[(info.numParams + 1)...(info.numParams + 1 + info.numDiscrs)]
+        discrs        := args[info.numParams + 1 : info.numParams + 1 + info.numDiscrs]
         altNumParams  := info.altNumParams
-        alts          := args[(info.numParams + 1 + info.numDiscrs)...(info.numParams + 1 + info.numDiscrs + info.numAlts)]
-        remaining     := args[(info.numParams + 1 + info.numDiscrs + info.numAlts)...args.size]
+        alts          := args[info.numParams + 1 + info.numDiscrs : info.numParams + 1 + info.numDiscrs + info.numAlts]
+        remaining     := args[info.numParams + 1 + info.numDiscrs + info.numAlts : args.size]
       }
 
     if alsoCasesOn && isCasesOnRecursor (← getEnv) declName then
@@ -51,12 +51,12 @@ def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCases
       let .inductInfo info ← getConstInfo indName | return none
       let args := e.getAppArgs
       unless args.size >= info.numParams + 1 /- motive -/ + info.numIndices + 1 /- major -/ + info.numCtors do return none
-      let params     := args[*...info.numParams]
+      let params     := args[:info.numParams]
       let motive     := args[info.numParams]!
-      let discrs     := args[(info.numParams + 1)...(info.numParams + 1 + info.numIndices + 1)]
+      let discrs     := args[info.numParams + 1 : info.numParams + 1 + info.numIndices + 1]
       let discrInfos := .replicate (info.numIndices + 1) {}
-      let alts       := args[(info.numParams + 1 + info.numIndices + 1)...(info.numParams + 1 + info.numIndices + 1 + info.numCtors)]
-      let remaining  := args[(info.numParams + 1 + info.numIndices + 1 + info.numCtors)...*]
+      let alts       := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors]
+      let remaining  := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :]
       let uElimPos?  := if info.levelParams.length == declLevels.length then none else some 0
       let mut altNumParams := #[]
       for ctor in info.ctors do

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -403,8 +403,8 @@ def inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp := do
       let propAlts ← matcherApp.alts.mapM fun termAlt =>
         lambdaTelescope termAlt fun xs termAltBody => do
           -- We have alt parameters and parameters corresponding to the extra args
-          let xs1 := xs[*...(xs.size - nExtra)]
-          let xs2 := xs[(xs.size - nExtra)...xs.size]
+          let xs1 := xs[0 : xs.size - nExtra]
+          let xs2 := xs[xs.size - nExtra : xs.size]
           -- logInfo m!"altIH: {xs} => {altIH}"
           let altType ← inferType termAltBody
           for x in xs2 do

src/Lean/Meta/SizeOf.lean

@@ -128,10 +128,10 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
   let recInfo : RecursorVal ← getConstInfoRec recName
   forallTelescopeReducing recInfo.type fun xs _ =>
     let levelParams := recInfo.levelParams.tail! -- universe parameters for declaration being defined
-    let params := xs[*...recInfo.numParams]
-    let motiveFVars := xs[recInfo.numParams...(recInfo.numParams + recInfo.numMotives)]
-    let minorFVars := xs[recInfo.getFirstMinorIdx...(recInfo.getFirstMinorIdx + recInfo.numMinors)]
-    let indices := xs[recInfo.getFirstIndexIdx...(recInfo.getFirstIndexIdx + recInfo.numIndices)]
+    let params := xs[:recInfo.numParams]
+    let motiveFVars := xs[recInfo.numParams : recInfo.numParams + recInfo.numMotives]
+    let minorFVars := xs[recInfo.getFirstMinorIdx : recInfo.getFirstMinorIdx + recInfo.numMinors]
+    let indices := xs[recInfo.getFirstIndexIdx : recInfo.getFirstIndexIdx + recInfo.numIndices]
     let major := xs[recInfo.getMajorIdx]!
     let nat := mkConst ``Nat
     mkLocalInstances params fun localInsts =>
@@ -193,8 +193,8 @@ def mkSizeOfSpecLemmaName (ctorName : Name) : Name :=
 def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
   matchConstCtor ctorApp.getAppFn (fun _ => throwError "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo _ => do
     let ctorArgs     := ctorApp.getAppArgs
-    let ctorParams   := ctorArgs[*...ctorInfo.numParams]
-    let ctorFields   := ctorArgs[ctorInfo.numParams...*]
+    let ctorParams   := ctorArgs[:ctorInfo.numParams]
+    let ctorFields   := ctorArgs[ctorInfo.numParams:]
     let lemmaName  := mkSizeOfSpecLemmaName ctorInfo.name
     let lemmaInfo  ← getConstInfo lemmaName
     let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
@@ -229,7 +229,7 @@ private def recToSizeOf (e : Expr) : M Expr := do
     | none => throwUnexpected m!"expected recursor application {indentExpr e}"
     | some sizeOfName =>
       let args    := e.getAppArgs
-      let indices := args[info.getFirstIndexIdx...(info.getFirstIndexIdx + info.numIndices)]
+      let indices := args[info.getFirstIndexIdx : info.getFirstIndexIdx + info.numIndices]
       let major   := args[info.getMajorIdx]!
       return mkAppN (mkConst sizeOfName us.tail!) ((← read).params ++ (← read).localInsts ++ indices ++ #[major])
 
@@ -269,8 +269,8 @@ mutual
   /-- Construct proof of auxiliary lemma. See `mkSizeOfAuxLemma` -/
   private partial def mkSizeOfAuxLemmaProof (info : InductiveVal) (lhs : Expr) : M Expr := do
     let lhsArgs := lhs.getAppArgs
-    let sizeOfBaseArgs := lhsArgs[*...(lhsArgs.size - info.numIndices - 1)]
-    let indicesMajor := lhsArgs[(lhsArgs.size - info.numIndices - 1)...*]
+    let sizeOfBaseArgs := lhsArgs[:lhsArgs.size - info.numIndices - 1]
+    let indicesMajor := lhsArgs[lhsArgs.size - info.numIndices - 1:]
     let sizeOfLevels := lhs.getAppFn.constLevels!
     let rec
       /-- Auxiliary function for constructing an `_sizeOf_<idx>` for `ys`,
@@ -294,7 +294,7 @@ mutual
       let recName := mkRecName info.name
       let recInfo ← getConstInfoRec recName
       let r := mkConst recName (levelZero :: us)
-      let r := mkAppN r majorTypeArgs[*...info.numParams]
+      let r := mkAppN r majorTypeArgs[:info.numParams]
       forallBoundedTelescope (← inferType r) recInfo.numMotives fun motiveFVars _ => do
         let mut r := r
         -- Add motives
@@ -366,12 +366,12 @@ mutual
         let x := lhs.appArg!
         let xType ← whnf (← inferType x)
         matchConstInduct xType.getAppFn (fun _ => throwFailed) fun info _ => do
-          let params := xType.getAppArgs[*...info.numParams]
+          let params := xType.getAppArgs[:info.numParams]
           forallTelescopeReducing (← inferType (mkAppN xType.getAppFn params)) fun indices _ => do
             let majorType := mkAppN (mkAppN xType.getAppFn params) indices
             withLocalDeclD `x majorType fun major => do
               let lhsArgs := lhs.getAppArgs
-              let lhsArgsNew := lhsArgs[*...(lhsArgs.size - 1 - indices.size)] ++ indices ++ #[major]
+              let lhsArgsNew := lhsArgs[:lhsArgs.size - 1 - indices.size] ++ indices ++ #[major]
               let lhsNew := mkAppN lhs.getAppFn lhsArgsNew
               let rhsNew ← mkAppM ``SizeOf.sizeOf #[major]
               let eq ← mkEq lhsNew rhsNew
@@ -428,8 +428,8 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
   let us := ctorInfo.levelParams.map mkLevelParam
   let simpAttr ← ofExcept <| getAttributeImpl (← getEnv) `simp
   forallTelescopeReducing ctorInfo.type fun xs _ => do
-    let params := xs[*...ctorInfo.numParams]
-    let fields := xs[ctorInfo.numParams...*]
+    let params := xs[:ctorInfo.numParams]
+    let fields := xs[ctorInfo.numParams:]
     let ctorApp := mkAppN (mkConst ctorName us) xs
     mkLocalInstances params fun localInsts => do
       let lhs ← mkAppM ``SizeOf.sizeOf #[ctorApp]
@@ -490,9 +490,9 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
         for indTypeName in indInfo.all, fn in fns do
           let indInfo ← getConstInfoInduct indTypeName
           forallTelescopeReducing indInfo.type fun xs _ =>
-            let params := xs[*...indInfo.numParams]
+            let params := xs[:indInfo.numParams]
             withInstImplicitAsImplict params do
-              let indices := xs[indInfo.numParams...*]
+              let indices := xs[indInfo.numParams:]
               mkLocalInstances params fun localInsts => do
                 let us := indInfo.levelParams.map mkLevelParam
                 let indType := mkAppN (mkConst indTypeName us) xs

src/Lean/Meta/Tactic/Cases.lean

@@ -50,7 +50,7 @@ def generalizeTargetsEq (mvarId : MVarId) (motiveType : Expr) (targets : Array E
       forallTelescopeReducing motiveType fun targetsNew _ => do
         unless targetsNew.size ≥ targets.size do
           throwError "invalid number of targets #{targets.size}, motive only takes #{targetsNew.size}"
-        let targetsNewAtomic := targetsNew[*...targets.size]
+        let targetsNewAtomic := targetsNew[:targets.size]
         withNewEqs targets targetsNewAtomic fun eqs eqRefls => do
           let typeNew ← mvarId.getType
           let typeNew ← mkForallFVars eqs typeNew

src/Lean/Meta/Tactic/Constructor.lean

@@ -37,7 +37,7 @@ def _root_.Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId :
       fun _ us cval => do
         if cval.numFields < 2 then
           throwTacticEx `exists mvarId "constructor must have at least two fields"
-        let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[*...cval.numParams]
+        let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.numParams]
         let ctorType ← inferType ctor
         let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.numFields-2))
         let f := mkAppN ctor mvars

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -58,7 +58,7 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
     unless motive.isFVar do
       throwError "expected resulting type of eliminator to be an application of one of its parameters (the motive):{indentExpr type}"
     let targets  := motiveArgs.takeWhile (·.isFVar)
-    let complexMotiveArgs := motiveArgs[targets.size...*]
+    let complexMotiveArgs := motiveArgs[targets.size:]
     let motiveType ← inferType motive
     forallTelescopeReducing motiveType fun motiveParams motiveResultType => do
       unless motiveParams.size == motiveArgs.size do

src/Lean/Meta/Tactic/FunInd.lean

@@ -243,7 +243,7 @@ def tell (x : Expr) : M Unit := fun xs => pure ((), xs.push x)
 def localM (f : Array Expr → MetaM (Array Expr)) (act : M α) : M α := fun xs => do
   let n := xs.size
   let (b, xs') ← act xs
-  pure (b, xs'[*...n] ++ (← f xs'[n...*]))
+  pure (b, xs'[:n] ++ (← f xs'[n:]))
 
 def localMapM (f : Expr → MetaM Expr) (act : M α) : M α :=
   localM (·.mapM f) act
@@ -1021,9 +1021,9 @@ where doRealize (inductName : Name) := do
           forallTelescope (← inferType e').bindingDomain! fun xs goal => do
             if xs.size ≠ 2 then
               throwError "expected recursor argument to take 2 parameters, got {xs}" else
-            let targets : Array Expr := xs[*...1]
+            let targets : Array Expr := xs[:1]
             let genIH := xs[1]!
-            let extraParams := xs[2...*]
+            let extraParams := xs[2:]
             -- open body with the same arg
             let body ← instantiateLambda body targets
             lambdaTelescope1 body fun oldIH body => do
@@ -1142,7 +1142,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
       if 5 ≤ args.size then
         let scrut := args[3]!
         let k := args[4]!
-        let extra := args[5...*]
+        let extra := args[5:]
         if scrut.isAppOfArity ``PSigma.mk 4 then
           let #[_, _, x, y] := scrut.getAppArgs | unreachable!
           let e' := (k.beta #[x, y]).beta extra
@@ -1151,7 +1151,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
     if f.isConstOf ``PSigma.fst then
       if h : 3 ≤ args.size then
         let scrut := args[2]
-        let extra := args[3...*]
+        let extra := args[3:]
         if scrut.isAppOfArity ``PSigma.mk 4 then
           let #[_, _, x, _y] := scrut.getAppArgs | unreachable!
           let e' := x.beta extra
@@ -1159,7 +1159,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
     if f.isConstOf ``PSigma.snd then
       if h : 3 ≤ args.size then
         let scrut := args[2]
-        let extra := args[3...*]
+        let extra := args[3:]
         if scrut.isAppOfArity ``PSigma.mk 4 then
           let #[_, _, _x, y] := scrut.getAppArgs | unreachable!
           let e' := y.beta extra
@@ -1177,7 +1177,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
         let scrut := args[3]!
         let k₁ := args[4]!
         let k₂ := args[5]!
-        let extra := args[6...*]
+        let extra := args[6:]
         if scrut.isAppOfArity ``PSum.inl 3 then
           let e' := (k₁.beta #[scrut.appArg!]).beta extra
           return .visit e'
@@ -1187,9 +1187,9 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
     -- Look for _unary redexes
     if f.isConstOf eqnInfo.declNameNonRec then
       if h : args.size ≥ eqnInfo.fixedParamPerms.numFixed + 1 then
-        let xs := args[*...eqnInfo.fixedParamPerms.numFixed]
+        let xs := args[:eqnInfo.fixedParamPerms.numFixed]
         let packedArg := args[eqnInfo.fixedParamPerms.numFixed]
-        let extraArgs := args[eqnInfo.fixedParamPerms.numFixed<...*]
+        let extraArgs := args[eqnInfo.fixedParamPerms.numFixed+1:]
         let some (funIdx, ys) := eqnInfo.argsPacker.unpack packedArg
           | throwError "Unexpected packedArg:{indentExpr packedArg}"
         let args' := eqnInfo.fixedParamPerms.perms[funIdx]!.buildArgs xs ys
@@ -1311,14 +1311,14 @@ where doRealize inductName := do
       let recInfo ← getConstInfoRec (mkRecName indName)
       if args.size < recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives then
         throwError "insufficient arguments to .brecOn:{indentExpr body}"
-      let brecOnArgs    : Array Expr := args[*...recInfo.numParams]
-      let _brecOnMotives : Array Expr := args[recInfo.numParams...(recInfo.numParams + recInfo.numMotives)]
-      let brecOnTargets : Array Expr := args[(recInfo.numParams + recInfo.numMotives)...
-        (recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1)]
-      let brecOnMinors  : Array Expr := args[(recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1)...
-        (recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives)]
-      let brecOnExtras  : Array Expr := args[(recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 +
-        recInfo.numMotives)...*]
+      let brecOnArgs    : Array Expr := args[:recInfo.numParams]
+      let _brecOnMotives : Array Expr := args[recInfo.numParams:recInfo.numParams + recInfo.numMotives]
+      let brecOnTargets : Array Expr := args[recInfo.numParams + recInfo.numMotives :
+        recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1]
+      let brecOnMinors  : Array Expr := args[recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 :
+        recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives]
+      let brecOnExtras  : Array Expr := args[ recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 +
+        recInfo.numMotives:]
       unless brecOnTargets.all (·.isFVar) do
         throwError "the indices and major argument of the brecOn application are not variables:{indentExpr body}"
       unless brecOnExtras.all (·.isFVar) do
@@ -1418,9 +1418,9 @@ where doRealize inductName := do
               let minor' ← forallTelescope goal fun xs goal => do
                 unless xs.size ≥ numTargets do
                   throwError ".brecOn argument has too few parameters, expected at least {numTargets}: {xs}"
-                let targets : Array Expr := xs[*...numTargets]
+                let targets : Array Expr := xs[:numTargets]
                 let genIH := xs[numTargets]!
-                let extraParams := xs[numTargets<...*]
+                let extraParams := xs[numTargets+1:]
                 -- open body with the same arg
                 let body ← instantiateLambda brecOnMinor targets
                 lambdaTelescope1 body fun oldIH body => do
@@ -1541,19 +1541,19 @@ where
       e.withApp fun f args => do
         if f.isConst then
           if let some matchInfo ← getMatcherInfo? f.constName! then
-            for scrut in args[matchInfo.getFirstDiscrPos...matchInfo.getFirstAltPos] do
+            for scrut in args[matchInfo.getFirstDiscrPos:matchInfo.getFirstAltPos] do
               if let some i := xs.idxOf? scrut then
                 modify (·.set! i true)
-            for alt in args[matchInfo.getFirstAltPos...matchInfo.arity] do
+            for alt in args[matchInfo.getFirstAltPos:matchInfo.arity] do
               go xs alt
         if f.isConstOf ``letFun then
-          for arg in args[3...4] do
+          for arg in args[3:4] do
             go xs arg
         if f.isConstOf ``ite || f.isConstOf ``dite then
-          for arg in args[3...5] do
+          for arg in args[3:5] do
             go xs arg
         if f.isConstOf ``cond then
-          for arg in args[2...4] do
+          for arg in args[2:4] do
             go xs arg
 
 /--

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -236,7 +236,7 @@ private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
     unless a.isAppOf ctorVal.name do
       -- TODO: remove ctorVal.numFields after update stage0
       if (← isExtTheorem inductVal.name) || ctorVal.numFields == 0 then
-        let params := aType.getAppArgs[*...inductVal.numParams]
+        let params := aType.getAppArgs[:inductVal.numParams]
         let mut ctorApp := mkAppN (mkConst ctorVal.name us) params
         for j in [: ctorVal.numFields] do
           let mut proj ← mkProjFn ctorVal us params j a

src/Lean/Meta/Tactic/Lets.lean

@@ -169,7 +169,7 @@ def withDeclInContext (fvarId : FVarId) (k : M α) : M α := do
     -- Is either pre-existing or already added.
     k
   else if let some idx := decls.findIdx? (·.decl.fvarId == fvarId) then
-    withEnsuringDeclsInContext decls[*...(idx+1)] k
+    withEnsuringDeclsInContext decls[0:idx+1] k
   else
     k
 
@@ -282,7 +282,7 @@ where
   extractApp (f : Expr) (args : Array Expr) : M Expr := do
     let cfg ← read
     if f.isConstOf ``letFun && args.size ≥ 4 then
-      extractApp (mkAppN f args[*...4]) args[4...*]
+      extractApp (mkAppN f args[0:4]) args[4:]
     else
       let f' ← extractCore fvars f
       if cfg.implicits then

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -935,8 +935,8 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
   let mut extraArgs := #[]
   if e.getAppNumArgs > numArgs then
     let args := e.getAppArgs
-    e := mkAppN e.getAppFn args[*...numArgs]
-    extraArgs := args[numArgs...*].toArray
+    e := mkAppN e.getAppFn args[:numArgs]
+    extraArgs := args[numArgs:].toArray
   if (← withSimpMetaConfig <| isDefEq lhs e) then
     let mut modified := false
     for i in c.hypothesesPos do

src/Lean/Meta/Tactic/Split.lean

@@ -146,12 +146,12 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
             let altNew ← lambdaTelescope alt fun xs body => do
               if xs.size < altNumParams || xs.size < numDiscrEqs then
                 throwError "internal error in `split` tactic: encountered an unexpected `match` expression alternative\nthis error typically occurs when the `match` expression has been constructed using meta-programming."
-              let body ← mkLambdaFVars xs[altNumParams...*] (← mkNewTarget body)
-              let ys  := xs[*...(altNumParams - numDiscrEqs)]
+              let body ← mkLambdaFVars xs[altNumParams:] (← mkNewTarget body)
+              let ys  := xs[:altNumParams - numDiscrEqs]
               if numDiscrEqs == 0 then
                 mkLambdaFVars ys body
               else
-                let altEqs := xs[(altNumParams - numDiscrEqs)...altNumParams]
+                let altEqs := xs[altNumParams - numDiscrEqs : altNumParams]
                 withNewAltEqs matcherInfo eqs altEqs fun altEqsNew subst => do
                   let body := body.replaceFVars altEqs subst
                   mkLambdaFVars (ys++altEqsNew) body

src/Lean/Meta/WHNF.lean

@@ -125,7 +125,7 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorTypeI := majorType.getAppFn
   if !majorTypeI.isConstOf recVal.getMajorInduct then
     return major
-  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams...*].any Expr.hasExprMVar then
+  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
     return major
   else do
     let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure major
@@ -523,7 +523,7 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
   let mut f ← instantiateValueLevelParams constInfo declLevels
   if (← getTransparency) matches .instances | .reducible then
     f ← unfoldNestedDIte f
-  let auxApp := mkAppN f args[*...prefixSz]
+  let auxApp := mkAppN f args[0:prefixSz]
   let auxAppType ← inferType auxApp
   forallBoundedTelescope auxAppType info.numAlts fun hs _ => do
     let auxApp ← whnfMatcher (mkAppN auxApp hs)
@@ -532,7 +532,7 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
     for h in hs do
       if auxAppFn == h then
         let result := mkAppN args[i]! auxApp.getAppArgs
-        let result := mkAppN result args[(prefixSz + info.numAlts)...args.size]
+        let result := mkAppN result args[prefixSz + info.numAlts:args.size]
         return ReduceMatcherResult.reduced result.headBeta
       i := i + 1
     return ReduceMatcherResult.stuck auxApp

src/Lean/MetavarContext.lean

@@ -960,7 +960,7 @@ instance : MonadHashMapCacheAdapter ExprStructEq Expr M where
 /-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
 private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl := Id.run do
   let mut d : LocalDecl := lctx.getFVar! xs[0]!
-  for x in xs[1...*] do
+  for x in xs[1:] do
     if x.isFVar then
       let curr := lctx.getFVar! x
       if curr.index < d.index then

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -273,11 +273,11 @@ def needsExplicit (f : Expr) (numArgs : Nat) (paramKinds : Array ParamKind) : Bo
     -- Error calculating ParamKinds, so return `true` to be safe
     paramKinds.size < numArgs
     -- One of the supplied parameters isn't explicit
-    || paramKinds[*...numArgs].any (fun param => !param.bInfo.isExplicit)
+    || paramKinds[:numArgs].any (fun param => !param.bInfo.isExplicit)
     -- The next parameter is implicit or inst implicit
     || (numArgs < paramKinds.size && paramKinds[numArgs]!.bInfo matches .implicit | .instImplicit)
     -- One of the parameters after the supplied parameters is explicit but not regular explicit.
-    || paramKinds[numArgs...*].any (fun param => param.bInfo.isExplicit && !param.isRegularExplicit)
+    || paramKinds[numArgs:].any (fun param => param.bInfo.isExplicit && !param.isRegularExplicit)
 
 /--
 Delaborates a function application in explicit mode.
@@ -382,7 +382,7 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
         else
           pure none
       if let some obj := obj? then
-        let isFirst := args[*...fieldIdx].all (· matches .skip)
+        let isFirst := args[0:fieldIdx].all (· matches .skip)
         -- Clear the `obj` argument from `args`.
         let args' := args.set! fieldIdx .skip
         let mut head : Term ← `($obj.$(mkIdentFrom fnStx field))
@@ -483,7 +483,7 @@ def useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool
 
   -- If any of the next parameters is explicit but has an optional value or is an autoparam, fall back to explicit mode.
   -- This is necessary since these are eagerly processed when elaborating.
-  if paramKinds[numArgs...*].any fun param => param.bInfo.isExplicit && !param.isRegularExplicit then return true
+  if paramKinds[numArgs:].any fun param => param.bInfo.isExplicit && !param.isRegularExplicit then return true
 
   return false
 
@@ -633,7 +633,7 @@ def delabStructureInstance : Delab := do
       from the same type family (think `Sigma`), but for now users can write a custom delaborator in such instances.
     -/
     let bis ← forallTelescope s.type fun xs _ => xs.mapM (·.fvarId!.getBinderInfo)
-    if explicit then guard <| bis[s.numParams...*].all (·.isExplicit)
+    if explicit then guard <| bis[s.numParams:].all (·.isExplicit)
     let (_, args) ← withBoundedAppFnArgs s.numFields
       (do return (0, #[]))
       (fun (i, args) => do
@@ -653,7 +653,7 @@ def delabStructureInstance : Delab := do
     -/
     let .const _ levels := (← getExpr).getAppFn | failure
     let args := (← getExpr).getAppArgs
-    let params := args[*...s.numParams]
+    let params := args[0:s.numParams]
     let (_, fields) ← collectStructFields s.induct levels params #[] {} s
     let tyStx? : Option Term ← withType do
       if ← getPPOption getPPStructureInstanceType then delab else pure none
@@ -795,7 +795,7 @@ partial def delabAppMatch : Delab := whenNotPPOption getPPExplicit <| whenPPOpti
         -- Need to reduce since there can be `let`s that are lifted into the matcher type
         forallTelescopeReducing (← getExpr) fun afterParams _ => do
           -- Skip motive and discriminators
-          let alts := Array.ofSubarray afterParams[(1 + st.discrs.size)...*]
+          let alts := Array.ofSubarray afterParams[1 + st.discrs.size:]
           -- Visit minor premises
           alts.mapIdxM fun idx alt => do
             let altTy ← inferType alt

src/Lean/Server/FileWorker/InlayHints.lean

@@ -168,7 +168,7 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) :
     s.oldInlayHints.filter fun (ihi : Elab.InlayHintInfo) =>
       ! invalidOldInlayHintsRange.contains ihi.position
   let newInlayHints : Array Elab.InlayHintInfo ← (·.2) <$> StateT.run (s := #[]) do
-    for s in snaps[oldFinishedSnaps...*] do
+    for s in snaps[oldFinishedSnaps:] do
       s.infoTree.visitM' (postNode := fun ci i _ => do
         let .ofCustomInfo i := i
           | return

src/Lean/Structure.lean

@@ -474,7 +474,7 @@ partial def mergeStructureResolutionOrders [Monad m] [MonadEnv m]
     let (good, name) ← selectParent resOrders
 
     unless good || relaxed do
-      let conflicts := resOrders |>.filter (·[1...*].any (· == name)) |>.map (·[0]!) |>.qsort Name.lt |>.eraseReps
+      let conflicts := resOrders |>.filter (·[1:].any (· == name)) |>.map (·[0]!) |>.qsort Name.lt |>.eraseReps
       defects := defects.push {
         isDirectParent := parentNames.contains name
         badParent := name
@@ -495,8 +495,8 @@ where
       let hi := resOrders.size - n'
       for i in [0 : hi] do
         let parent := resOrders[i]![0]!
-        let consistent resOrder := resOrder[1...*].all (· != parent)
-        if resOrders[*...<i].all consistent && resOrders[i<...hi].all consistent then
+        let consistent resOrder := resOrder[1:].all (· != parent)
+        if resOrders[0:i].all consistent && resOrders[i+1:hi].all consistent then
           return (n' == 0, parent)
     -- unreachable, but correct default:
     return (false, resOrders[0]![0]!)

src/Lean/Syntax.lean

@@ -379,7 +379,7 @@ partial def reprint (stx : Syntax) : Option String := do
         -- this visit the first arg twice, but that should hardly be a problem
         -- given that choice nodes are quite rare and small
         let s0 ← reprint args[0]!
-        for arg in args[1...*] do
+        for arg in args[1:] do
           let s' ← reprint arg
           guard (s0 == s')
     | _ => pure ()

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -8,8 +8,6 @@ prelude
 import Lean.Linter.UnusedVariables
 import Lean.Server.Utils
 import Lean.Widget.InteractiveGoal
-import Init.Data.Slice.Array.Basic
-import Init.Data.Array.Subarray.Split
 
 namespace Lean.Widget
 open Lsp Server
@@ -165,7 +163,7 @@ where
             | none     => child
         let blockSize := ctx.bind (maxTraceChildren.get? ·.opts)
           |>.getD maxTraceChildren.defValue
-        let children := chopUpChildren data.cls blockSize children[*...*]
+        let children := chopUpChildren data.cls blockSize children.toSubarray
         pure (.lazy children)
       else
         pure (.strict (← children.mapM (go nCtx ctx)))
@@ -181,8 +179,8 @@ where
   chopUpChildren (cls : Name) (blockSize : Nat) (children : Subarray MessageData) :
       Array MessageData :=
     if blockSize > 0 && children.size > blockSize + 1 then  -- + 1 to make idempotent
-      let more := chopUpChildren cls blockSize (children.drop blockSize)
-      (children.take blockSize).toArray.push <|
+      let more := chopUpChildren cls blockSize children[blockSize:]
+      children[:blockSize].toArray.push <|
         .trace { collapsed := true, cls }
           f!"{children.size - blockSize} more entries..." more
     else children