Zulip Chat Archive
Stream: lean4
Topic: partial & while
Locria Cyber (Dec 16 2022 at 23:37):
The following code passes typecheck.
def a := do
while true do
IO.println ""
partial def b : IO Unit := do
IO.println ""
b
Locria Cyber (Dec 16 2022 at 23:37):
why isn't a marked partial?
Adam Topaz (Dec 16 2022 at 23:51):
The while loop uses docs4#Lean.Loop.forIn under the hood, which is also marked with partial.
Last updated: May 02 2025 at 03:31 UTC