Zulip Chat Archive
Stream: lean4
Topic: Coercion from String to Substring?
François G. Dorais (Aug 03 2023 at 16:44):
This has probably been discussed before but a quick search didn't find anything.
I think the world would be more wonderful if there was a coercion from String to Substring. Is there a reason why there isn't one?
Last updated: May 02 2025 at 03:31 UTC