From 4c972ba0d63ddacef6b032b8e3e014cd62fc16f6 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Tue, 18 Nov 2025 10:31:31 +0000 Subject: [PATCH] fix: add missing `s!` in `UInt64.fromJson?` (#11237) This PR fixes the error thrown by `UInt64.fromJson?` and `USize.fromJson?` to use the missing `s!`. --- src/Lean/Data/Json/FromToJson/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Data/Json/FromToJson/Basic.lean b/src/Lean/Data/Json/FromToJson/Basic.lean index afdb7e4e39..60e79038b7 100644 --- a/src/Lean/Data/Json/FromToJson/Basic.lean +++ b/src/Lean/Data/Json/FromToJson/Basic.lean @@ -155,7 +155,7 @@ def bignumToJson (n : Nat) : Json := protected def _root_.USize.fromJson? (j : Json) : Except String USize := do let n ← bignumFromJson? j if n ≥ USize.size then - throw "value '{j}' is too large for `USize`" + throw s!"value '{j}' is too large for `USize`" return USize.ofNat n instance : FromJson USize where @@ -167,7 +167,7 @@ instance : ToJson USize where protected def _root_.UInt64.fromJson? (j : Json) : Except String UInt64 := do let n ← bignumFromJson? j if n ≥ UInt64.size then - throw "value '{j}' is too large for `UInt64`" + throw s!"value '{j}' is too large for `UInt64`" return UInt64.ofNat n instance : FromJson UInt64 where