From 6a1cc7d6b8aa96c2e89da348df7f45a15224d84c Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 22 Oct 2025 08:35:51 +0200 Subject: [PATCH] chore: minor `String` improvements (#10891) This PR renames the cast functions on `String.ValidPos` for `set` and `modify` to adhere to the established naming convention. It also fixes two typos and very slighly tweaks the import graph, shortening the critical path by a negligible amount. --- src/Init/Data/String/Basic.lean | 14 +++++++------- src/Init/Data/ToString/Name.lean | 2 +- src/Init/System/IO.lean | 1 - src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- 4 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 6a081cffc5..98052fe7d2 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1674,7 +1674,7 @@ def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.ValidPos where isValid := pos.isValidForSlice.ofSlice @[simp] -theorem Slice.Pos.ofset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl) +theorem Slice.Pos.offset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl) @[simp] theorem rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.rawEndPos := by @@ -2538,14 +2538,14 @@ theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp : /-- Given a valid position in a string, obtain the corresponding position after setting a character on that string, provided that the position was before the changed position. -/ @[inline] -def ValidPos.setOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos) +def ValidPos.toSetOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.set c hp).ValidPos where offset := q.offset isValid := q.isValid.set_of_le hpq @[simp] -theorem ValidPos.offset_setOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} - {hpq : q ≤ p} : (q.setOfLE p c hp hpq).offset = q.offset := (rfl) +theorem ValidPos.offset_toSetOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} + {hpq : q ≤ p} : (q.toSetOfLE p c hp hpq).offset = q.offset := (rfl) /-- Replaces the character at position `p` in the string `s` with the result of applying `f` to that @@ -2568,14 +2568,14 @@ theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.ValidPos} {f : Char → /-- Given a valid position in a string, obtain the corresponding position after modifying a character in that string, provided that the position was before the changed position. -/ -def ValidPos.modifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char) +def ValidPos.toModifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char) (hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.modify f hp).ValidPos where offset := q.offset isValid := q.isValid.modify_of_le hpq @[simp] -theorem ValidPos.offset_modifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char} - {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.modifyOfLE p f hp hpq).offset = q.offset := (rfl) +theorem ValidPos.offset_toModifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char} + {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl) /-- Replaces the character at a specified position in a string with a new character. If the position is diff --git a/src/Init/Data/ToString/Name.lean b/src/Init/Data/ToString/Name.lean index 7b136f0d76..0b93be9ddb 100644 --- a/src/Init/Data/ToString/Name.lean +++ b/src/Init/Data/ToString/Name.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura and Sebastian Ullrich module prelude -public import Init.Data.String.Extra +public import Init.Data.String.Basic /-! Here we give the. implementation of `Name.toString`. There is also a private implementation in diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index c7f9318166..aa6b9c3d4c 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -9,7 +9,6 @@ prelude public import Init.System.IOError public import Init.System.FilePath public import Init.Data.Ord.UInt -public import Init.Data.String.Extra public section diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 780d8d7b40..0371e03d3d 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -26,7 +26,7 @@ This module finds lexicographic termination measures for well-founded recursion. Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures (e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations -until it finds one where all proof obligations go through with the given tactic (`decerasing_by`), +until it finds one where all proof obligations go through with the given tactic (`decreasing_by`), if given, or the default `decreasing_tactic`. For mutual recursion, a single measure is not just one parameter, but one from each recursive