Nonterminating IO in lean?

Stream: general

[Alex J. Best]

For IO, you can use unsafe def.
You may want to ask the first question in the #lean4 stream, I'm not sure if the answer will be any different in theory, but it might be more likely to be seen by someone who can answer there

[Erika Su]

thanks! i shall ask accordingly.

[Sebastian Ullrich]

Please don't use unsafe for this :) . The correct replacement is partial as mentioned in https://leanprover.github.io/lean4/doc/lean3changes.html#the-meta-keyword.

[Sebastian Ullrich]

(or use repeat!)

[Alex J. Best]

Oops! My bad, I did a quick grep on mathlib4 and found unsafe def.*IO only and no partial def.*IO and assumed based on that.