CODEWITHSUNDEEP
string-interpolationlean
Random Citizen
Random Citizen

Reputation: 1376

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.

Upvotes: 1

Views: 45

Answers (1)

Random Citizen
Random Citizen

Reputation: 1376

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

Upvotes: 1

Related Questions