如何在Lean 4中将字符串转换为整数？

Lean 4提供了带错误处理的字符串转整数函数，你可以结合模式匹配处理输入可能的无效情况，以下是修改后的代码：

def main : IO Unit := do
    let stdin ← IO.getStdin
    let stdout ← IO.getStdout
  
    stdout.putStrLn "Pick a number between 0 and 38"
    let input ← stdin.getLine 
    let trimmedInput := input.trim  -- 移除换行符与前后空格
    match trimmedInput.toNat? with
    | some n => 
        if n >= 0 && n <= 38 then
            stdout.putStrLn s!"You picked the number {n}"
        else
            stdout.putStrLn "Number is out of the 0-38 range!"
    | none => stdout.putStrLn "Invalid input! Please enter a valid natural number."

关键说明： #

• input.trim：用户输入的字符串会包含末尾的换行符（由getLine读取），用trim可以清除换行符和意外的前后空格，避免转换失败。
• String.toNat?：尝试将字符串转换为自然数（Nat类型），返回Option Nat——转换成功时返回some n，输入非有效数字时返回none。如果需要处理负数，可替换为String.toInt?（返回Option Int）。
• 模式匹配：通过match分支分别处理转换成功和失败的场景，给用户明确的反馈。

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