Zulip Chat Archive

Stream: lean4

Topic: How to get input from keyboard?

dudubao2007 (Jun 23 2022 at 14:44):

How to get input from keyboard in Lean4? (IO String)
What is the typeclass that provides read : String -> a?

Henrik Böving (Jun 23 2022 at 14:47):

There is no typeclass but there is docs4#IO.getStdin which has a way to read from it.

Arthur Paulino (Jun 23 2022 at 14:51):

let input ← (← (← IO.getStdin).getLine)

dudubao2007 (Jun 23 2022 at 14:57):

Sorry, but that can't compile.

Henrik Böving (Jun 23 2022 at 15:01):

Arthur did one left arrow too much, apart from that it's fine.

Arthur Paulino (Jun 23 2022 at 15:03):

Yeah, this is the fixed version: let input : String ← (← IO.getStdin).getLine, sorry

dudubao2007 (Jun 23 2022 at 15:04):

Thank you very much. :rose:

Christian Pehle (Jun 23 2022 at 15:05):

A complete program that echos input would be

def main (argv : List String) : IO Unit := do
  let input := (← (← IO.getStdin).getLine)
  IO.print input

Mauricio Collares (Jun 23 2022 at 15:13):

Henrik Böving said:

There is no typeclass but there is docs4#IO.getStdin which has a way to read from it.

I'm curious about @dudubao2007's second question. I guess you can do input.toInt? to get an Option Int. But there is no standard "inverse" to show or repr in general, if I understand correctly.

Henrik Böving (Jun 23 2022 at 15:17):

We don't have haskel style read right now no, although that will most likely be in scope of a standard librayr for the future.

dudubao2007 (Jun 24 2022 at 01:49):

Thank you for your great help.

dudubao2007 (Jun 24 2022 at 02:03):

The result of "toInt?" is always none because of the ending '\n'. Is there a version of "toInt" that ignores spaces?

Sebastian Ullrich (Jun 24 2022 at 07:29):

Use String.trim

Last updated: Dec 20 2023 at 11:08 UTC