Stream: Beginner Questions

Topic: Convert a char to nat

view this post on Zulip Bilel Ghorbel (Jul 09 2021 at 08:10):

I am looking for a bijective function that converts a char to nat, and hopefully its reverse function

view this post on Zulip Lukas Stevens (Jul 09 2021 at 08:17):

How is this supposed to work? A char is just defined as 8 booleans in Isabelle.

view this post on Zulip Robert Soeldner (Jul 09 2021 at 08:20):

Cant u use char_of and of_char https://isabelle.in.tum.de/library/HOL/HOL/String.html

Last updated: Oct 25 2025 at 20:21 UTC