diff --git a/tests/lean/run/125.lean b/tests/lean/run/125.lean
index 71e066b80f..5191687e56 100644
--- a/tests/lean/run/125.lean
+++ b/tests/lean/run/125.lean
@@ -14,8 +14,8 @@ instance FooElems  : HasElems Foo  := ⟨(elems Bool).map mk1 ++ (elems Bool).ma
 
 def fooRepr (foo : Foo) :=
 match foo with
-| mk1 b => "OH " ++ toString b
-| mk2 b => "DR " ++ toString b
+| mk1 b => s!"OH {b}"
+| mk2 b => s!"DR {b}"
 
 instance : HasRepr Foo := ⟨fooRepr⟩
 
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index 020fd07b9c..2ec102f9e5 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -24,7 +24,7 @@ IO.println b;
 pure (s+a);
 
 def myPrint {α} [HasToString α] (a : α) : IO Unit :=
-IO.println (">> " ++ toString a)
+IO.println s!">> {a}"
 
 def h₂ (x : Nat) : StateT Nat IO Nat := do
 let a ← h 1;        -- liftM inserted here
@@ -131,10 +131,10 @@ if x > 0 then
   y := 3*y
   z := z + (← get) + (← get)
 if x < (← get) then
-  IO.println (">> " ++ toString y)
+  IO.println s!">> {y}"
   return y
 else
-  IO.println ("++ " ++ toString z)
+  IO.println s!"++ {z}"
   return y+z
 
 set_option trace.Elab.do true
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index 988b55b632..82264e9c36 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -4,7 +4,7 @@ def f (x : Nat) : IO Nat := do
 IO.println "hello world"
 let aux (y : Nat) (z : Nat) : IO Nat := do
   IO.println "aux started"
-  IO.println ("y: " ++ toString y ++ ", z: " ++ toString z)
+  IO.println s!"y: {y}, z: {z}"
   pure (x+y)
 aux x
   (x + 1) -- It is part of the application since it is indented
@@ -19,7 +19,7 @@ aux x x;
 def g (xs : List Nat) : StateT Nat Id Nat := do
 if xs.isEmpty then
   xs := [← get]
-dbgTrace! ">>> xs: " ++ toString xs
+dbgTrace! s!">>> xs: {xs}"
 return xs.length
 
 #eval g [1, 2, 3] $.run' 10
@@ -54,7 +54,7 @@ for x in xs do
     break
   unless x % 2 == 1 do
     continue
-  dbgTrace! ">> x: " ++ toString x
+  dbgTrace! s!">> x: {x}"
 return sum
 
 #eval sumOdd [1, 2, 3, 4, 5, 6, 7, 9, 11, 101] 10
diff --git a/tests/lean/run/doNotation4.lean b/tests/lean/run/doNotation4.lean
index b5800f5c81..9d6e7a795a 100644
--- a/tests/lean/run/doNotation4.lean
+++ b/tests/lean/run/doNotation4.lean
@@ -54,7 +54,7 @@ catch
 def f4 (xs : List Nat) : M Nat := do
 let y := 0
 for x in xs do
-  IO.println ("x: " ++ toString x)
+  IO.println s!"x: {x}"
   try
     dec x
     y := y + x
@@ -69,7 +69,7 @@ get
 def f5 (xs : List Nat) : M Nat := do
 let y := 0
 for x in xs do
-  IO.println ("x: " ++ toString x)
+  IO.println s!"x: {x}"
   try
     dec x
     y := y + x