Thanks for pointing that out. My feeling is still “well yes, that’s technically true, but it still seems unnatural, and explosion is still the odd axiom out”.
Coq, for example, allows empty case expressions (for empty types), and I expect that other languages which double as proof assistants would support them as well… for the very purpose of satisfying explosion. General purpose languages like Haskell (and I just checked OCaml too) can seemingly overlook explosion/empty cases with few if any practical problems.
Thanks for pointing that out. My feeling is still “well yes, that’s technically true, but it still seems unnatural, and explosion is still the odd axiom out”.
Coq, for example, allows empty case expressions (for empty types), and I expect that other languages which double as proof assistants would support them as well… for the very purpose of satisfying explosion. General purpose languages like Haskell (and I just checked OCaml too) can seemingly overlook explosion/empty cases with few if any practical problems.