Zulip Chat Archive

Stream: general

Topic: Nonterminating IO in lean?

Alex J. Best (Oct 21 2022 at 15:25):

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 (Oct 21 2022 at 15:34):

thanks! i shall ask accordingly.

Sebastian Ullrich (Oct 21 2022 at 15:34):

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 (Oct 21 2022 at 15:35):

(or use repeat!)

Alex J. Best (Oct 21 2022 at 15:36):

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.

Last updated: Dec 20 2023 at 11:08 UTC