File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
src/Lean/Data/Json/FromToJson Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -155,7 +155,7 @@ def bignumToJson (n : Nat) : Json :=
155155protected def _root_.USize.fromJson? (j : Json) : Except String USize := do
156156 let n ← bignumFromJson? j
157157 if n ≥ USize.size then
158- throw "value '{j}' is too large for `USize`"
158+ throw s! "value '{ j} ' is too large for `USize`"
159159 return USize.ofNat n
160160
161161instance : FromJson USize where
@@ -167,7 +167,7 @@ instance : ToJson USize where
167167protected def _root_.UInt64.fromJson? (j : Json) : Except String UInt64 := do
168168 let n ← bignumFromJson? j
169169 if n ≥ UInt64.size then
170- throw "value '{j}' is too large for `UInt64`"
170+ throw s! "value '{ j} ' is too large for `UInt64`"
171171 return UInt64.ofNat n
172172
173173instance : FromJson UInt64 where
You can’t perform that action at this time.
0 commit comments