## Stream: general

### Topic: auto derive has_to_string

#### Zesen Qian (Jul 21 2018 at 20:49):

RT, something like this in lean?

#### Mario Carneiro (Jul 21 2018 at 20:56):

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

#### Simon Hudon (Jul 21 2018 at 20:59):

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 (Jul 21 2018 at 21:04):

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

#### Zesen Qian (Jul 21 2018 at 21:05):

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

#### Simon Hudon (Jul 21 2018 at 21:05):

You write @[derive has_reflect] above your type definition

#### Mario Carneiro (Jul 21 2018 at 21:06):

I meant write a derive handler

#### Zesen Qian (Jul 21 2018 at 21:07):

@Simon Hudon very cool, thanks.

You're welcome

#### Simon Hudon (Jul 21 2018 at 21:10):

@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

Last updated: May 12 2021 at 23:13 UTC