bump to nightly-2026-03-25

HumanEvalLean/HumanEval15.lean

@@ -3,7 +3,7 @@ import Std.Data.Iterators.Producers.Range
 import Std
 
 def stringSequence (n : Nat) : String :=
-  Std.Iter.intercalateString.{0} " " ((0...=n).iter.map (String.toSlice ∘ Nat.repr))
+  Std.Iter.intercalateString " " ((0...=n).iter.map (String.toSlice ∘ Nat.repr))
 
 example : stringSequence 0 = "0" := by native_decide
 example : stringSequence 3 = "0 1 2 3" := by native_decide

HumanEvalLean/HumanEval27.lean

@@ -20,10 +20,6 @@ theorem toList_flipCase {string : String} : (flipCase string).toList = string.to
 
 namespace Char
 
-@[simp]
-theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 theorem isUpper_flipCase {c : Char} : c.flipCase.isUpper ↔ c.isLower := by
   grind [flipCase, isUpper, isLower, toUpper, toLower]
 

HumanEvalLean/HumanEval50.lean

@@ -12,10 +12,6 @@ def encodeShift (s : String) : String :=
 def decodeShift (s : String) : String :=
   s.map Char.unshiftByFive
 
-@[simp]
-theorem Char.toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 theorem Char.toNat_ofNat_of_isValidChar {n : Nat} (h : n.isValidChar) : (Char.ofNat n).toNat = n := by
   simp [ofNat, h, ofNatAux]
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-03-24
+leanprover/lean4:nightly-2026-03-25