Zulip Chat Archive
Stream: new members
Topic: unsafe casts in meta land?
Scott Morrison (Jan 04 2019 at 05:03):
In a meta function, is there some way to do "unsafe casts"?
Mario Carneiro (Jan 04 2019 at 05:20):
unchecked_cast
Mario Carneiro (Jan 04 2019 at 05:21):
it's just cast with a fake proof
Mario Carneiro (Jan 04 2019 at 05:21):
But it's not recommended. There are very few safe but type incorrect casts
Mario Carneiro (Jan 04 2019 at 05:22):
and the ones that exist already have names, like unquot
Last updated: Dec 20 2023 at 11:08 UTC