Lean4字符串插值能否自定义十六进制格式化？

Lean4的s!字符串插值语法本身不支持类似Rust中通过:指定格式化参数的功能，要实现将UInt8类型的颜色分量格式化为带前导零的两位十六进制数，需要自定义格式化逻辑，具体步骤如下：

1. 实现单个UInt8的格式化函数
   先写一个辅助函数，把UInt8转换为两位带前导零的十六进制字符串：

   def UInt8.toHex2 (n : UInt8) : String :=
     let hexStr := Nat.reprHex n.toNat
     -- 若长度不足2则补前导零，否则直接返回
     if hexStr.length < 2 then "0" ++ hexStr else hexStr
   

   这里利用Nat.reprHex将UInt8转为小写十六进制字符串，再通过判断长度补零，确保最终结果始终是两位字符。

2. 修改Color的to_hex方法
   在字符串插值中调用上面的格式化函数，替换原本直接插入UInt8的写法：

   structure Color where
     r : UInt8
     g : UInt8
     b : UInt8
   
   def Color.to_hex : Color → String
     | {r, g, b} => s!"#{r.toHex2}{g.toHex2}{b.toHex2}"
   
   def color : Color := ⟨ 0, 7, 255 ⟩
   
   #eval color.to_hex -- 输出 "#0007ff"
   #guard color.to_hex = "#0007ff" -- 符合预期
   

如果需要支持大写十六进制，可以将Nat.reprHex替换为Nat.reprHexUpper，调整辅助函数即可。

内容的提问来源于stack exchange，提问作者Random Citizen