我在Lean (v4.22.0) 中构建一个递归下降解析器，需要从一个典型的十进制浮点数 String 中解析出一个 Float。

我说的字符串类型示例可能是 "3.141592"、"-2.17" 等等。我会在C 程序中使用 strtod，在Rust程序中使用 str::parse。

我不能通过类型强制转换来完成这个任务：

#eval ("3.14" : Float)

Type mismatch
  "3.14"
has type
  String
but is expected to have type
  Float

我已经在 loogle 查找类似 "String.toFloat" 和 "Float.ofString" 的函数，以及任何签名为 "String -> Float" 或 "String -> Option Float" 的函数。我也查阅了Lean参考手册中关于 [Strings] 和 [Floats] 的部分。我确信Lean中没有像C 和Rust那样提供这一功能的单一函数。

我也考虑过使用FFI从 C标准库调用 strtod，但Lean页面关于外部函数接口的第一句话是“当前接口是为Lean内部使用而设计，应视为不稳定。”

Lean 4是否提供一种受支持的方式（例如在 mathlib 中）将一个十进制的 String 解析为 Float？ 如果没有，调用Lean解析器是否是预期的方法？

解决方案

我找不到标准库中像 String.toFloat 这样的函数，但你可以使用Lean自身用于解析浮点字面量的现有函数来实现它：

def String.toFloat? (s : String) : Option Float := do
  let mut s := s
  let mut sign := false
  if let some s' := s.dropPrefix? '-' then
    sign := true
    s := s'.copy
  if let some (n, esign, e) := Lean.Syntax.decodeScientificLitVal? s then
    let res := Float.ofScientific n esign e
    return if sign then -res else res
  else if let some n := Lean.Syntax.decodeNatLitVal? s then
    let res := Float.ofNat n
    return if sign then -res else res
  else none

#eval "3.14".toFloat?
#eval "abc".toFloat?

值得注意的是，Lean.Syntax.decodeScientificLitVal? 在Lean内部用于解析浮点字面量，如 0.1、.37、13.、24e5、1.25e-25 等；而 Lean.Syntax.decodeNatLitVal? 用于解析自然数（即 0、1 等）。要将结果转换为实际的浮点数，可以使用 Float.ofScientific 和 Float.ofNat。再加上一些对前导负号的处理，这可以处理诸如 -3、2.5e7、-2.e-9、8.97、-0 等情况。如果你还想处理无穷大或NaN，可以把它们作为特殊情况来添加。