non_exhaustive · Ltac2 · Zulip Chat Archive

Stream: Ltac2

Topic: non_exhaustive

Gaëtan Gilbert (Dec 05 2023 at 13:36):

Would something like this be useful for ltac2? https://doc.rust-lang.org/reference/attributes/type_system.html#the-non_exhaustive-attribute

I think that's a very, very useful tool to have but I am not sure how the idea of a rust crate would be mapped to Ltac2. The crucial point is that the defining crate itself doesn't have to add _ cases. If that cannot easily be recreated in Ltac2 I don't see a benefit over making the enum extensible to begin with.

Pierre-Marie Pédrot (Dec 05 2023 at 14:19):

I don't think that the crucial point is about the defining crate, it's just a QoL syntax. It's not critical to have to handle unknown cases even in the scope where you have control over the type, at worst you lose a little bit of safety. The interest is to force the users to have this default check.

Michael Soegtrop (Dec 05 2023 at 14:33):

I can imagine that this would be useful to write user extensible tactics, e.g. in Princeton VST. In some cases one would have to extend some enum or record data types for such extensions.

Janno (Dec 05 2023 at 14:38):

But extensible enums already force users to handle the default case, don't they? What's the difference to non_exhaustive without the QoL feature of skipping the default case in the defining crate/module?