Lean4 string interpolation: Possible to format as hex?

Is it possible to customize the formatting when using string interpolation with Lean4?

More precise: I want to format using hexadecimal digits and add zeros as padding.

Minimal example (Same example in Lean 4 Web):

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

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

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

Coming from other languages like Rust I would have expected to use some sort separator like : and add formatting information on the right side of that.

But that does not work (the colon has already a different meaning in Lean 4) and neither the documentation nor the reference give more information.

Solution

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