Reports

Even if string interpolation itself does not accept formatting parameters, it's not as bad as it might seem:

String interpolation in Lean 4 accepts arbitrary expression. So instead of having to remember a special syntax for formatting inside string interpolation you can just call a function doing the formatting.

Lean4 already provides a method for the given example (format UInt8 values using two hex digits no matter the value): BitVec.toHex

To keep the example small, I've just added a tiny method:

def UInt8.toHex (x : UInt8) : String := x.toBitVec.toHex

Now the example passes:

def UInt8.toHex (x : UInt8) : String := x.toBitVec.toHex

structure Color where
  r : UInt8
  g : UInt8
  b : UInt8

def Color.to_hex : Color → String
  | {r, g, b} => s!"#{r.toHex}{g.toHex}{b.toHex}"

def color : Color := ⟨ 0, 7, 255 ⟩

#eval color.to_hex
-- #guard color.to_hex = "#07255" -- *NOT* what I want
#guard color.to_hex = "#0007ff" -- What I want

Lean 4 Web Link

79350067