Zulip Chat Archive
Stream: lean4
Topic: undefined in Lean4
Chris Hughes (Dec 14 2022 at 13:04):
What is the equivalent of Lean3's unsafe def undefined in Lean4?
Mario Carneiro (Dec 14 2022 at 13:13):
lcProof works for proofs
Mario Carneiro (Dec 14 2022 at 13:13):
for other stuff you can use unsafeCast but it will usually cause a segfault
Mario Carneiro (Dec 14 2022 at 13:15):
there is also lcUnreachable which works for any type
Mario Carneiro (Dec 14 2022 at 13:16):
if the type is inhabited you should prefer panic!
Last updated: Dec 20 2023 at 11:08 UTC