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: Dec 20 2023 at 11:08 UTC