Trimming \n from getLine

Stream: new members

[Max]

I'm trying to write the classic guessing game in Lean4. But I can't convert the input I've read to a Nat, since it contains a trailing newline. This is my code:

def main : IO Unit := do
  let random <- IO.rand 1 100
  IO.println "I'm thinking of a random number between 1 and 100, try and guess it!"
  let stdin <- IO.getStdin
  let guess_str <- stdin.getLine
  match guess_str.toNat? with
  | some guess => IO.println s!"Your input: {guess}"
  | none => IO.println s!"'{guess_str}' is not a Nat"

results in

'3
' is not a Nat

How do I get rid of the newline?

[Max]

(And tips on how to improve my code otherwise are welcome too obviously)

[Alex J. Best]

Does the function trimRight do what you want https://github.com/leanprover/lean4/blob/e4995ce8ba86d4f0a08c61e3ea5545178d6d2fb8/src/Init/Data/String/Basic.lean#L530

[Max]

Oh, yep, it does,! I got match guess_str.trimRight.toNat? with ... now which works. Thanks!