various to_strings

Stream: general

[Edward Ayers]

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!

[Sean Leather]

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

[Edward Ayers]

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

[Sean Leather]

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.