auto derive has_to_string

Stream: general

[Zesen Qian]

RT, something like this in lean?

[Mario Carneiro]

No, I don't think this one has a derive handler, although you could totally write one

[Simon Hudon]

If you don't mind going into meta-land, you can derive has_reflect for your type and use the following to just pretty-print the Lean expression that corresponds to a value of your type:

meta def to_string' {α : Type*} [has_reflect α] (x : α) : string :=
(to_fmt (reflect x)).to_string

[Zesen Qian]

has_reflect asks me to provide a expr for every value? Not sure how to do it for my type.

[Zesen Qian]

@Mario Carneiro yeah, it's just a very long type.

[Simon Hudon]

You write @[derive has_reflect] above your type definition

[Mario Carneiro]

I meant write a derive handler

[Zesen Qian]

@Simon Hudon very cool, thanks.

[Simon Hudon]

You're welcome

[Simon Hudon]

@Mario Carneiro Such a derive handler seems like a lot of work but I'm wondering if piggy backing on top of has_reflect might help us be extra lazy