Zulip Chat Archive

Stream: lean4

Topic: return from repeat


Cole Shepherd (Dec 02 2022 at 06:20):

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 (Dec 02 2022 at 07:16):

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 (Dec 02 2022 at 08:46):

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

Mario Carneiro (Dec 02 2022 at 08:55):

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 (Dec 02 2022 at 08:56):

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

Last updated: Dec 20 2023 at 11:08 UTC