Zulip Chat Archive

Stream: lean4

Topic: deriving ToString?

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?

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.

Jason Gross (Mar 22 2021 at 14:31):

Ah, great, thanks!

Last updated: May 02 2025 at 03:31 UTC