Terse code

Stream: lean4

[Cole Shepherd]

How would I combine these three lines, executing in the IO monad, into one?

let input <- stdin.getLine
let guessAsStr := input.dropRightWhile Char.isWhitespace
let guess? := String.toNat? guessAsStr

[Adam Topaz]

Lean has do notation that should work here

[Cole Shepherd]

These lines are actually already in a ‘do’ block. I’m trying to figure out how to eliminate the two intermediate variables

[Adam Topaz]

can you provide a #mwe ?

[Scott Morrison]

Does

let guess? := String.toNat? <| (<- stdin.getLine).dropRightWhile Char.isWhitespace

work?

[Adam Topaz]

Yeah I assume a mwe is something like this

def foo : IO Unit := do
  let stdin ← getStdin
  let guessAsStr := String.toNat? <| (← stdin.getLine).dropRightWhile Char.isWhitespace

[Adam Topaz]

I think this should have the same behavior (with a bit more ascii art)

let guessAsStr ← String.toNat? <$> (String.dropRightWhile · Char.isWhitespace) <$> stdin.getLine

[Scott Morrison]

I find the (← f) syntax in Lean 4 so much easier to read/write/understand than "ascii art" (<$> and friends).