Zulip Chat Archive
Stream: new members
Topic: Which import to have HasToString?
Francesco Stiffoni (Apr 17 2021 at 15:12):
Sorry for the dummy question, in Lean 4 which import I have to use to have HasToString ?
Mario Carneiro (Apr 17 2021 at 15:13):
HasToString was renamed to ToString
Last updated: May 02 2025 at 03:31 UTC