From 6e538c35dd6737c4baea874fe337ce50b3b0d424 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 27 Jun 2025 20:52:07 +0200 Subject: [PATCH] refactor: migrate all usages of old slice notation (#9000) This PR replaces all usages of `[:]` slice notation in `src` with the new `[...]` notation in production code, tests and comments. The underlying implementation of the `Subarray` functions stays the same. Notation cheat sheet: * `*...*` is the doubly-unbounded range. * `*...a` or `*... Array/Iterator.lean} | 9 +- src/Init/Data/Stream.lean | 6 +- src/Init/Data/Vector/Basic.lean | 4 +- src/Init/NotationExtra.lean | 5 +- src/Lean/Compiler/LCNF/ElimDeadBranches.lean | 4 +- src/Lean/Compiler/LCNF/InferType.lean | 4 +- src/Lean/Compiler/LCNF/MonoTypes.lean | 4 +- src/Lean/Compiler/LCNF/PrettyPrinter.lean | 2 +- src/Lean/Compiler/LCNF/Probing.lean | 4 +- src/Lean/Compiler/LCNF/ReduceArity.lean | 4 +- src/Lean/Compiler/LCNF/Simp/DiscrM.lean | 2 +- src/Lean/Compiler/LCNF/Simp/JpCases.lean | 6 +- src/Lean/Compiler/LCNF/Simp/Main.lean | 10 +- src/Lean/Compiler/LCNF/Specialize.lean | 4 +- src/Lean/Compiler/LCNF/ToDecl.lean | 4 +- src/Lean/Compiler/LCNF/ToLCNF.lean | 12 +- src/Lean/Compiler/LCNF/ToMono.lean | 4 +- src/Lean/Data/FuzzyMatching.lean | 2 +- src/Lean/Elab/App.lean | 4 +- src/Lean/Elab/BuiltinNotation.lean | 4 +- src/Lean/Elab/ComputedFields.lean | 10 +- src/Lean/Elab/Declaration.lean | 2 +- src/Lean/Elab/DefView.lean | 12 +- src/Lean/Elab/Deriving/BEq.lean | 2 +- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/Deriving/ToExpr.lean | 4 +- src/Lean/Elab/Deriving/Util.lean | 6 +- src/Lean/Elab/ErrorExplanation.lean | 2 +- src/Lean/Elab/Inductive.lean | 2 +- src/Lean/Elab/Level.lean | 4 +- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/MutualInductive.lean | 10 +- src/Lean/Elab/PatternVar.lean | 2 +- src/Lean/Elab/PreDefinition/Eqns.lean | 2 +- src/Lean/Elab/PreDefinition/FixedParams.lean | 4 +- .../Elab/PreDefinition/Structural/BRecOn.lean | 4 +- .../PreDefinition/Structural/FindRecArg.lean | 4 +- .../Structural/IndGroupInfo.lean | 2 +- .../PreDefinition/Structural/IndPred.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Fix.lean | 4 +- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 4 +- .../Elab/PreDefinition/WF/PackMutual.lean | 4 +- .../Elab/PreDefinition/WF/Preprocess.lean | 2 +- src/Lean/Elab/Print.lean | 2 +- src/Lean/Elab/Quotation.lean | 2 +- src/Lean/Elab/SetOption.lean | 2 +- src/Lean/Elab/StructInst.lean | 4 +- src/Lean/Elab/Structure.lean | 4 +- src/Lean/Elab/Syntax.lean | 2 +- .../Tactic/BVDecide/Frontend/BVDecide.lean | 2 +- src/Lean/Elab/Tactic/BuiltinTactic.lean | 4 +- src/Lean/Elab/Tactic/Conv/Congr.lean | 10 +- src/Lean/Elab/Tactic/Ext.lean | 10 +- src/Lean/Elab/Tactic/Induction.lean | 12 +- src/Lean/Elab/Tactic/Omega/Frontend.lean | 4 +- src/Lean/Elab/Tactic/RCases.lean | 4 +- src/Lean/Elab/Tactic/Try.lean | 6 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Environment.lean | 2 +- src/Lean/Meta/CollectMVars.lean | 2 +- src/Lean/Meta/CongrTheorems.lean | 4 +- src/Lean/Meta/Constructions/BRecOn.lean | 16 +- .../Meta/Constructions/NoConfusionLinear.lean | 2 +- src/Lean/Meta/Constructions/RecOn.lean | 6 +- src/Lean/Meta/DiscrTree.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 10 +- src/Lean/Meta/IndPredBelow.lean | 36 ++--- src/Lean/Meta/InferType.lean | 4 +- src/Lean/Meta/Injective.lean | 2 +- src/Lean/Meta/LazyDiscrTree.lean | 2 +- src/Lean/Meta/LetToHave.lean | 2 +- src/Lean/Meta/Match/MatchEqs.lean | 18 +-- src/Lean/Meta/Match/MatcherApp/Basic.lean | 14 +- src/Lean/Meta/Match/MatcherApp/Transform.lean | 4 +- src/Lean/Meta/SizeOf.lean | 32 ++-- src/Lean/Meta/Tactic/Cases.lean | 2 +- src/Lean/Meta/Tactic/Constructor.lean | 2 +- src/Lean/Meta/Tactic/ElimInfo.lean | 2 +- src/Lean/Meta/Tactic/FunInd.lean | 48 +++--- src/Lean/Meta/Tactic/Grind/Internalize.lean | 2 +- src/Lean/Meta/Tactic/Lets.lean | 4 +- src/Lean/Meta/Tactic/Simp/Main.lean | 4 +- src/Lean/Meta/Tactic/Split.lean | 6 +- src/Lean/Meta/WHNF.lean | 6 +- src/Lean/MetavarContext.lean | 2 +- .../PrettyPrinter/Delaborator/Builtins.lean | 14 +- src/Lean/Server/FileWorker/InlayHints.lean | 2 +- src/Lean/Structure.lean | 6 +- src/Lean/Syntax.lean | 2 +- src/Lean/Widget/InteractiveDiagnostic.lean | 8 +- src/Std/Data/DHashMap/Internal/Defs.lean | 2 +- src/Std/Data/Iterators/Producers/Range.lean | 2 +- tests/bench/liasolver.lean | 2 +- tests/lean/run/305.lean | 2 +- tests/lean/run/ExprLens.lean | 2 +- tests/playground/deriving.lean | 2 +- 104 files changed, 457 insertions(+), 416 deletions(-) create mode 100644 src/Init/Data/Range/Polymorphic/Iterators.lean create mode 100644 src/Init/Data/Slice/Array/Basic.lean rename src/Init/Data/Slice/{Array.lean => Array/Iterator.lean} (79%) diff --git a/src/Init/Data/Array/QSort/Basic.lean b/src/Init/Data/Array/QSort/Basic.lean index 1723e2ce9f..070aaa9eb2 100644 --- a/src/Init/Data/Array/QSort/Basic.lean +++ b/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+1]` in-place using `lt` to compare elements. +`qsort as lt lo hi` sorts the subarray `as[lo...=hi]` 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. diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 2927c40737..0cfc5f89a3 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/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 [size] + simp only [size, ge_iff_le] 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 [size] at this + simp only [size] at this rw [Nat.add_comm] exact Nat.add_lt_of_lt_sub this s.array[s.start + i.val] diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index ffa5fa53ed..c19bf11c21 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -7,7 +7,6 @@ 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 diff --git a/src/Init/Data/Range/Polymorphic/Basic.lean b/src/Init/Data/Range/Polymorphic/Basic.lean index 370af75d89..d9552300cc 100644 --- a/src/Init/Data/Range/Polymorphic/Basic.lean +++ b/src/Init/Data/Range/Polymorphic/Basic.lean @@ -6,34 +6,10 @@ Authors: Paul Reichert module prelude -import Init.Data.Range.Polymorphic.RangeIterator -import Init.Data.Iterators.Combinators.Attach - -open Std.Iterators +import Init.Data.Range.Polymorphic.PRange 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. @@ -70,25 +46,6 @@ 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. @@ -101,100 +58,6 @@ 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 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 - theorem le_upper_of_mem {sl α} [LE α] [DecidableLE α] [SupportsLowerBound sl α] {a : α} {r : PRange ⟨sl, .closed⟩ α} (h : a ∈ r) : a ≤ r.upper := h.2 diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean new file mode 100644 index 0000000000..a1a336f90a --- /dev/null +++ b/src/Init/Data/Range/Polymorphic/Iterators.lean @@ -0,0 +1,151 @@ +/- +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 diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index 851d9c3182..0fc7686c03 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/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.PRange -import all Init.Data.Range.Polymorphic.RangeIterator import all Init.Data.Range.Polymorphic.Basic +import all Init.Data.Range.Polymorphic.RangeIterator +import all Init.Data.Range.Polymorphic.Iterators import all Init.Data.Iterators.Consumers.Loop /-! diff --git a/src/Init/Data/Slice.lean b/src/Init/Data/Slice.lean index cd1102591c..bfa05334f2 100644 --- a/src/Init/Data/Slice.lean +++ b/src/Init/Data/Slice.lean @@ -9,7 +9,8 @@ prelude import Init.Data.Slice.Basic import Init.Data.Slice.Notation import Init.Data.Slice.Operations -import Init.Data.Slice.Array +import Init.Data.Slice.Array.Basic +import Init.Data.Slice.Array.Iterator /-! # Polymorphic slices diff --git a/src/Init/Data/Slice/Array/Basic.lean b/src/Init/Data/Slice/Array/Basic.lean new file mode 100644 index 0000000000..833e849d50 --- /dev/null +++ b/src/Init/Data/Slice/Array/Basic.lean @@ -0,0 +1,27 @@ +/- +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... 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 diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean index 95ae15423d..4d51ee6911 100644 --- a/src/Lean/Compiler/LCNF/InferType.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/MonoTypes.lean b/src/Lean/Compiler/LCNF/MonoTypes.lean index d144036a24..f5dfa4eed0 100644 --- a/src/Lean/Compiler/LCNF/MonoTypes.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/PrettyPrinter.lean b/src/Lean/Compiler/LCNF/PrettyPrinter.lean index 8b64541fbc..499b182bfd 100644 --- a/src/Lean/Compiler/LCNF/PrettyPrinter.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/Probing.lean b/src/Lean/Compiler/LCNF/Probing.lean index c55fed0674..659e843b52 100644 --- a/src/Lean/Compiler/LCNF/Probing.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/ReduceArity.lean b/src/Lean/Compiler/LCNF/ReduceArity.lean index 8b35c7e54b..77d6b7cfb3 100644 --- a/src/Lean/Compiler/LCNF/ReduceArity.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean index 3b855b4b15..66eab280f7 100644 --- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean +++ b/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) diff --git a/src/Lean/Compiler/LCNF/Simp/JpCases.lean b/src/Lean/Compiler/LCNF/Simp/JpCases.lean index 930dd4e438..c82a9ed593 100644 --- a/src/Lean/Compiler/LCNF/Simp/JpCases.lean +++ b/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+1] ++ fields ++ args[targetParamIdx+1:] + args[*...=targetParamIdx] ++ fields ++ args[targetParamIdx<...*] else - args[:targetParamIdx] ++ fields ++ args[targetParamIdx+1:] + args[*...targetParamIdx] ++ fields ++ args[targetParamIdx<...*] /-- 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 => diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index e956ec4906..c989c79ac3 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 8b77861b16..88d87f2ebd 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean index d8de591308..852d52a855 100644 --- a/src/Lean/Compiler/LCNF/ToDecl.lean +++ b/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) diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 25533c79eb..030ab1c61b 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/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) diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index 1b82a500a4..1fb1636ee4 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/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 diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index e9cc41ba36..26b50ab542 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/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+1] and word[:j+1] assuming that pattern[i] misses at word[j] (k = 0, i.e. + between the substrings pattern[*...=i] and word[*...j] 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 diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 3846cecf1e..d958e6ef6e 100644 --- a/src/Lean/Elab/App.lean +++ b/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[0:elimInfo.motivePos] do + for x in xs[*...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 diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 966018249b..4257f98183 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/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[0:numExplicitFields-1].toArray.push newLast + let newArgs := args[*...(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}") diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean index 4177811b46..e5d3bf6d45 100644 --- a/src/Lean/Elab/ComputedFields.lean +++ b/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+1].toArray, - xs[numIndices+1]!, xs[numIndices+2:].toArray) + let (indices, major, minors) := (xs[1...=numIndices].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]))) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 77d4645e59..f12b8e7d6a 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/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[0:i], elems[i:elems.size]) + some (elems[*...i], elems[i...elems.size]) else none -- a `mutual` block containing only preamble commands is not a valid `mutual` block loop 0 diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 7a74c02d1a..553100a97b 100644 --- a/src/Lean/Elab/DefView.lean +++ b/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 := diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 981fa71f3e..d13dc4f0c1 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/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) diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 171ec7a939..f78546518e 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/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 diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean index 489f486f5d..21f7aaf85c 100644 --- a/src/Lean/Elab/Deriving/ToExpr.lean +++ b/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 diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 29f925ee14..214d556f9d 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/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) diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean index 9833cb13fc..d8400e765b 100644 --- a/src/Lean/Elab/ErrorExplanation.lean +++ b/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[0:stx.getNumArgs - 1]) + stx.setArgs (stx.getArgs[*...(stx.getNumArgs - 1)]) else stx let partialId := span[span.getNumArgs - 2] diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 81ba07d309..e92517a8f3 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/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. diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 5f9c56e001..2868a9cca8 100644 --- a/src/Lean/Elab/Level.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index f623e5557c..4e94721ea7 100644 --- a/src/Lean/Elab/Match.lean +++ b/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)) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 8a186dad9e..f4f0ca78bf 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/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 diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 0e5770a457..f0887b4dc5 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index b501ce966e..7825ee1754 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/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 _ diff --git a/src/Lean/Elab/PreDefinition/FixedParams.lean b/src/Lean/Elab/PreDefinition/FixedParams.lean index dc359df977..7123551673 100644 --- a/src/Lean/Elab/PreDefinition/FixedParams.lean +++ b/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? diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 1ab0df3bf0..7831031879 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index c2c4c6f1d6..85c18f0ee4 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/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[0:indInfo.numParams] - let indIndices : Array Expr := indArgs[indInfo.numParams:] + let indParams : Array Expr := indArgs[*...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 diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean index 3bec2fa2df..620dd17edf 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean index 51be0e27da..13a22a270e 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean +++ b/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" diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index 2a4b5ee91d..d7ad8d3a21 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/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+1:].toArray.mapM (loop F)) + return mkAppN r (← args[fixedPrefixSize<...*].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) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 72dfc110a9..09c41aa21a 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/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[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p] + xs[*...(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)) diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean index e11f4d5cc6..af465a6e2c 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean index a43ac2823f..0f6bec5046 100644 --- a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean +++ b/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. diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index db5e66cbb0..a6ddc86bb3 100644 --- a/src/Lean/Elab/Print.lean +++ b/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 diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 0b9de00173..af8d7ed157 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/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)) diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean index 93208abb25..54701e9a71 100644 --- a/src/Lean/Elab/SetOption.lean +++ b/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[0:3])) + addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...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 } diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index dc7897f643..afec44d7ec 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/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+1:] + return TransformStep.visit <| mkAppN arg args[projInfo.numParams<...*] return TransformStep.continue Meta.transform e (post := postVisit) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 794b04fdff..b49314d878 100644 --- a/src/Lean/Elab/Structure.lean +++ b/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) diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 7a03db3e4f..bc4483bf46 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/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) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 9aaa9d856c..91cf98da35 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/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, diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 91cf208e06..f572d27238 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/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] diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index d55a242a0e..0794d864ba 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/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[0:idx], xs[idx:]) + return (mkAppN f xs[*...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[0:idx], xs[idx:]) + return (mkAppN f xs[*...idx], xs[idx...*]) def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit := do if i == 0 then diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index 7f65640cbe..b79f921857 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/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[0:startIdx] do + for fvar in args[*...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 diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index ccbbd9d7b6..1551280bba 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 955c2b229c..2a489ddec5 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/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+1:].toArray.toList + let tail ← mkListLit (.const ``Int []) atoms[n<...*].toArray.toList let lem := .str ``LinearCombo s!"coordinate_eval_{n}" - mkEqSymm (mkAppN (.const lem []) (atoms[:n+1].toArray.push tail)) + mkEqSymm (mkAppN (.const lem []) (atoms[*...=n].toArray.push tail)) else let atoms ← atomsCoeffs let n := toExpr n diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean index 3ea8a666fa..b367dd78dd 100644 --- a/src/Lean/Elab/Tactic/RCases.lean +++ b/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)) diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index 423c434865..a6cb16ac98 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 446ee9da0d..5e4c59f966 100644 --- a/src/Lean/Elab/Term.lean +++ b/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?` diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 89ffd3dd86..871eae7e0b 100644 --- a/src/Lean/Environment.lean +++ b/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 #[] } diff --git a/src/Lean/Meta/CollectMVars.lean b/src/Lean/Meta/CollectMVars.lean index 13d07a47b7..d5d98e073c 100644 --- a/src/Lean/Meta/CollectMVars.lean +++ b/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) diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 5018e68138..2670e5ac0b 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/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) diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean index 3d65ac6d7a..c3c06c9246 100644 --- a/src/Lean/Meta/Constructions/BRecOn.lean +++ b/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 diff --git a/src/Lean/Meta/Constructions/NoConfusionLinear.lean b/src/Lean/Meta/Constructions/NoConfusionLinear.lean index 16e47d3115..be0dc7cd7b 100644 --- a/src/Lean/Meta/Constructions/NoConfusionLinear.lean +++ b/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 diff --git a/src/Lean/Meta/Constructions/RecOn.lean b/src/Lean/Meta/Constructions/RecOn.lean index 26c528c19e..e0403382d3 100644 --- a/src/Lean/Meta/Constructions/RecOn.lean +++ b/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 diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index a95b43ca8c..afe2a9ce24 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/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 diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index ca067af61d..2c32ac00b1 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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[0:i].any fun prevArg => prevArg == arg then + if args[*...i].any fun prevArg => prevArg == arg then useFOApprox args else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then useFOApprox args diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index d35631a7c0..db2d66ca58 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -81,7 +81,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 +100,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 +137,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 +178,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 +195,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 +331,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 +387,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 +426,14 @@ partial def mkBelowMatcher lambdaTelescope alt fun xs t => do let oldFVars := oldLhs.fvarDecls.toArray let fvars := lhs.fvarDecls.toArray.map (·.toExpr) - let xs := + let xs : Array Expr := -- 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:] + | 0, _+1 => xs[1...*].toArray | _, _ => 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 +483,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 +555,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 diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 150b00bb8b..c992409d34 100644 --- a/src/Lean/Meta/InferType.lean +++ b/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[*... 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 diff --git a/src/Lean/Meta/Match/MatcherApp/Basic.lean b/src/Lean/Meta/Match/MatcherApp/Basic.lean index 5fb9fa0dd5..762ec475be 100644 --- a/src/Lean/Meta/Match/MatcherApp/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index 2ab42bd4b0..1d7198c0e7 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/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[0 : xs.size - nExtra] - let xs2 := xs[xs.size - nExtra : xs.size] + let xs1 := xs[*...(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 diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 35b5564674..396f65ebef 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/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_` 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 diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index a2c24fc403..b9b616151c 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Constructor.lean b/src/Lean/Meta/Tactic/Constructor.lean index da98ce00ac..ac8fb3ae96 100644 --- a/src/Lean/Meta/Tactic/Constructor.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index 1e3c45deb3..01eedf52d9 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index d5ed78720d..2530ef121a 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/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+1:] + let extraArgs := args[eqnInfo.fixedParamPerms.numFixed<...*] 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+1:] + let extraParams := xs[numTargets<...*] -- 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 /-- diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index d5e0272edf..4c588f13ad 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Lets.lean b/src/Lean/Meta/Tactic/Lets.lean index 90cf2f670f..48cbf0df2f 100644 --- a/src/Lean/Meta/Tactic/Lets.lean +++ b/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[0:idx+1] k + withEnsuringDeclsInContext decls[*...(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[0:4]) args[4:] + extractApp (mkAppN f args[*...4]) args[4...*] else let f' ← extractCore fvars f if cfg.implicits then diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 3deb41d74c..6daa3d839d 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 95e15b89a6..bcf442ef97 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/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 diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 6244316743..2491a8d286 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/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[0:prefixSz] + let auxApp := mkAppN f args[*...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 diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 25e7beda45..c40f118147 100644 --- a/src/Lean/MetavarContext.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index e8b844f412..0a93fac586 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/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[0:fieldIdx].all (· matches .skip) + let isFirst := args[*...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[0:s.numParams] + let params := args[*...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 diff --git a/src/Lean/Server/FileWorker/InlayHints.lean b/src/Lean/Server/FileWorker/InlayHints.lean index 90c7fc55da..7d0a49076f 100644 --- a/src/Lean/Server/FileWorker/InlayHints.lean +++ b/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 diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index b2791c7adf..d5f68c6088 100644 --- a/src/Lean/Structure.lean +++ b/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[0:i].all consistent && resOrders[i+1:hi].all consistent then + let consistent resOrder := resOrder[1...*].all (· != parent) + if resOrders[*... pure () diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 66a1207394..59578755a0 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -8,6 +8,8 @@ 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 @@ -163,7 +165,7 @@ where | none => child let blockSize := ctx.bind (maxTraceChildren.get? ·.opts) |>.getD maxTraceChildren.defValue - let children := chopUpChildren data.cls blockSize children.toSubarray + let children := chopUpChildren data.cls blockSize children[*...*] pure (.lazy children) else pure (.strict (← children.mapM (go nCtx ctx))) @@ -179,8 +181,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[blockSize:] - children[:blockSize].toArray.push <| + let more := chopUpChildren cls blockSize (children.drop blockSize) + (children.take blockSize).toArray.push <| .trace { collapsed := true, cls } f!"{children.size - blockSize} more entries..." more else children diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index 438d6851fb..cb40861d9c 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -193,7 +193,7 @@ def expand [Hashable α] (data : { d : Array (AssocList α β) // 0 < d.size }) let nbuckets := data.size * 2 go 0 data ⟨Array.replicate nbuckets AssocList.nil, by simpa [nbuckets] using Nat.mul_pos hd Nat.two_pos⟩ where - /-- Inner loop of `expand`. Copies elements `source[i:]` into `target`, + /-- Inner loop of `expand`. Copies elements `source[i...*]` into `target`, destroying `source` in the process. -/ go (i : Nat) (source : Array (AssocList α β)) (target : { d : Array (AssocList α β) // 0 < d.size }) : diff --git a/src/Std/Data/Iterators/Producers/Range.lean b/src/Std/Data/Iterators/Producers/Range.lean index 6f12a67c91..b99bceedf8 100644 --- a/src/Std/Data/Iterators/Producers/Range.lean +++ b/src/Std/Data/Iterators/Producers/Range.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Paul Reichert -/ prelude -import Init.Data.Range.Polymorphic.Basic +import Init.Data.Range.Polymorphic.Iterators /-! # Range iterator diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean index 0fc8023695..e522256277 100644 --- a/tests/bench/liasolver.lean +++ b/tests/bench/liasolver.lean @@ -341,7 +341,7 @@ def main (args : List String) : IO UInt32 := do let nEquations ← header.ithVal 0 "amount of equations" let nVars ← header.ithVal 1 "amount of variables" let mut equations : HashMap Nat Equation := ∅ - for line in lines[1:] do + for line in lines[1...*] do let elems := line.splitOn.toArray let nTerms ← elems.ithVal 0 "amount of equation terms" let 0 ← elems.ithVal (elems.size - 1) "end of line symbol" diff --git a/tests/lean/run/305.lean b/tests/lean/run/305.lean index bdebaea140..4ea31620d2 100644 --- a/tests/lean/run/305.lean +++ b/tests/lean/run/305.lean @@ -22,7 +22,7 @@ namespace Cmd def subCmdByFullName? (c : Cmd) (fullName : Array String) : Option Cmd := do let mut c := c guard <| c.name = fullName.get? 0 - for subName in fullName[1:] do + for subName in fullName[1...*] do c ← c.subCmd? subName return c end Cmd diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean index b8a0f1f9fc..2d5e3f12f1 100644 --- a/tests/lean/run/ExprLens.lean +++ b/tests/lean/run/ExprLens.lean @@ -8,7 +8,7 @@ def Lean.LocalContext.subtract (Γ Δ : LocalContext) : Array Expr := -- have Δ = Γ ++ E let Δ := Δ.getFVars let Γ := Γ.getFVars - let E := Δ[:(Δ.size - Γ.size)] + let E := Δ[*...(Δ.size - Γ.size)] E.toArray def ExprTraversal := ∀{M : _} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadOptions M], (Pos → Expr → M Expr) → Pos → Expr → M Expr diff --git a/tests/playground/deriving.lean b/tests/playground/deriving.lean index d5076ea999..7791abf57c 100644 --- a/tests/playground/deriving.lean +++ b/tests/playground/deriving.lean @@ -198,7 +198,7 @@ def mkLocalInstanceLetDecls (ctx : Context) (argNames : Array Name) : TermElabM let auxFunName := ctx.auxFunNames[i] let currArgNames ← mkInductArgNames indVal let numParams := indVal.nparams - let currIndices := currArgNames[numParams:] + let currIndices := currArgNames[numParams...*] let binders ← mkImplicitBinders currIndices let argNamesNew := argNames[:numParams] ++ currIndices let indType ← mkInductiveApp indVal argNamesNew