while foo := f () do

Stream: lean4

[Locria Cyber]

def main : IO Unit := do
  let stdin <- IO.getStdin

  while let line := <- stdin.getLine; not line.isEmpty do
    IO.println line
    -- IO.println line
    pure ()

Shouldn't this work?

[Henrik Böving]

This is due to how it gets desugared i guess:

def main : IO Unit := do
  let stdin <- IO.getStdin
  while let line := (← stdin.getLine); not line.isEmpty do
    IO.println "hello"

#print main

def main : IO Unit :=
do
  let stdin ← liftM IO.getStdin
  let col := Lean.Loop.mk;
    forIn col PUnit.unit fun x r => do
      let a ← stdin.getLine
      if
            (let line := a;
              !String.isEmpty line) =
              true then
          do
          IO.println "hello"
          pure (ForInStep.yield PUnit.unit)
        else pure (ForInStep.done PUnit.unit)
  pure PUnit.unit

Whihc is because lean does not support the type of syntax you are going for (that is an if/while let + a condition) right now, however if i remember correctly @Sebastian Ullrich recently opened an issue about this and does want to add it.

[Locria Cyber]

I see
how do I see the desugared expression myself in Lean? special #command?

[Henrik Böving]

I just showed you above