Topic: Nonterminating IO in lean?
Alex J. Best (Oct 21 2022 at 15:25):
IO, you can use
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):
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: Aug 03 2023 at 10:10 UTC