Nontermating "do" blocks

Stream: new members

[Ayden Coughlin]

When reading about the "do" notation in the Lean manual, I started experimenting and noticed that you're able to write nonterminating functions without Lean complaining:

def loops : IO Unit := do
  while true do
    pure ()

Why are you not required to mark this function as "partial"?

[Mario Carneiro]

"partial" is not a viral marker, it is only used for definitions that are directly recursive, and implies that they cannot be unfolded

[Mario Carneiro]

There is a partial involved in defining while, but your code is only calling that definition so you have no direct recursion in your function (i.e. loops does not call itself)

[Mario Carneiro]

(the partial is in src#Lean.Loop.forIn)

[Ayden Coughlin]

I see. Thank you.

[Ayden Coughlin]

This concerns me a little bit. How can I be confident that my function terminates if it can depend on partial functions indirectly in this way? Also, are there alternatives to while and similar imperative-style constructs that are not partial (requiring some kind of manual proof of termination)?

[Mario Carneiro]

If you use tail-recursion, then you will have to prove termination manually, or use partial