return from repeat

Stream: lean4

[Cole Shepherd]

I'm trying to compile a function similar to the the one below as part of a larger program:

partial def repro : IO Nat := do
  repeat do
    let x := some 3

    match x with
      | some y => return y
      | none => IO.println ""

but I'm getting the compile error on line 2:

type mismatch, `for` has type
  PUnit : Sort ?u.505
but is expected to have type
  Nat : Type

How can I fix this? Thanks.

[Damiano Testa]

I'm not at a computer, but I think that lean would like an IO Nat also from the none branch of the match. IO.println "" may not qualify!

[Sebastian Ullrich]

No, it's the repeat that doesn't return Nat. There is no special support for "repeat without break" yet.

[Mario Carneiro]

and now this has got me interested in implementing it... but I'm not sure there is anyone remaining to review a PR to Do.lean at this point

[Mario Carneiro]

here's the workaround:

partial def repro : IO Nat := do
  let x := some 3

  match x with
    | some y => return y
    | none => IO.println ""; repro