From e9a8b965aa310f2600e7586885cc91168d7ee90c Mon Sep 17 00:00:00 2001
From: Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 09:21:55 +0100
Subject: [PATCH] fix: remove extra universe parameter
 from`Std.Iter.intercalateString` (#13092)

This PR fixes an issue where `Std.Iter.joinString` had an extra universe
parameter because of an `IteratorLoop` instance which was actually
unnecessary.
---
 src/Init/Data/String/Iter/Intercalate.lean | 4 ++--
 src/Init/Data/String/Lemmas/Iter.lean      | 7 +++----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/String/Iter/Intercalate.lean b/src/Init/Data/String/Iter/Intercalate.lean
index 414a5da70e..2c662d024d 100644
--- a/src/Init/Data/String/Iter/Intercalate.lean
+++ b/src/Init/Data/String/Iter/Intercalate.lean
@@ -17,7 +17,7 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
-public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)
 
@@ -25,7 +25,7 @@ public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α I
 Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
 -/
 @[inline]
-public def Iter.intercalateString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+public def Iter.intercalateString {α β : Type} [Iterator α Id β] [ToString β]
     (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
   it.map toString
     |>.fold (init := none) (fun
diff --git a/src/Init/Data/String/Lemmas/Iter.lean b/src/Init/Data/String/Lemmas/Iter.lean
index 34c659f770..62f4253a2e 100644
--- a/src/Init/Data/String/Lemmas/Iter.lean
+++ b/src/Init/Data/String/Lemmas/Iter.lean
@@ -18,14 +18,13 @@ namespace Std.Iter
 
 @[simp]
 public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β]
-    {it : Std.Iter (α := α) β} : it.joinString = String.join (it.toList.map toString) := by
+    [ToString β] {it : Std.Iter (α := α) β} :
+    it.joinString = String.join (it.toList.map toString) := by
   rw [joinString, String.join, ← foldl_toList, toList_map]
 
 @[simp]
 public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β] {s : String.Slice}
-    {it : Std.Iter (α := α) β} :
+    [ToString β] {s : String.Slice} {it : Std.Iter (α := α) β} :
     it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
   simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
   generalize s.copy = s