Zulip Chat Archive
Stream: general
Topic: char is_upper / to_upper etc
Johan Commelin (Apr 08 2019 at 19:01):
Are the functions that convert a char
to it's uppercase/lowercase sibling?
Simon Hudon (Apr 08 2019 at 19:03):
char.to_lower
and char.to_upper
should do it
Last updated: Dec 20 2023 at 11:08 UTC