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