Zulip Chat Archive

Stream: general

Topic: various to_strings


view this post on Zulip Edward Ayers (Oct 01 2018 at 11:18):

Hi all, when should I use the following typeclasses to display information?
- has_repr
- has_to_string
- has_to_format
- has_to_tactic_format -- the tactic version of has_to_format?
In particular, why bother having both has_repr and has_to_string?
Thanks!

view this post on Zulip Sean Leather (Oct 01 2018 at 11:20):

Some background: https://github.com/leanprover/lean/issues/1664

view this post on Zulip Edward Ayers (Oct 01 2018 at 11:23):

Ok, so they are exactly the same except with how they deal with chars and strings?

view this post on Zulip Sean Leather (Oct 01 2018 at 11:25):

Ok, so they are exactly the same except with how they deal with chars and strings?

I suppose so. I haven't looked into it myself.


Last updated: May 15 2021 at 00:39 UTC