I am looking for a bijective function that converts a char to nat, and hopefully its reverse function
How is this supposed to work? A char is just defined as 8 booleans in Isabelle.
Cant u use char_of
and of_char
https://isabelle.in.tum.de/library/HOL/HOL/String.html
Last updated: Dec 07 2024 at 16:22 UTC