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