CharToNat and NatToChar type families
Show, we need
CharToNat. And with
NatToChar to accompany it, we can also define promoted
These type families were originally part of !3598, but it is currently on hold because it’s unclear whether we want to add so many built-in definitions (and also because the author currently has no time to rebase it and clean it up, at least in time for the %9.2.1 release). However, now there’s a clear case for
NatToChar, so this ticket is to track their addition.
Patch here: !5258 (closed)