Zulip Chat Archive

Stream: lean4

Topic: deriving ToString?


view this post on Zulip Jason Gross (Mar 22 2021 at 14:19):

Is there a way to get a default ToString instance for structures/inductives all of whose constructors have arguments with ToString instances?

view this post on Zulip Leonardo de Moura (Mar 22 2021 at 14:28):

Jason Gross said:

Is there a way to get a default ToString instance for structures/inductives all of whose constructors have arguments with ToString instances?

We have deriving Repr. repr e produces a format object that is a "representation" for e. Repr is similar to Haskell's Show.

view this post on Zulip Jason Gross (Mar 22 2021 at 14:31):

Ah, great, thanks!


Last updated: May 07 2021 at 12:15 UTC