Zulip Chat Archive

Stream: general

Topic: auto derive has_to_string


view this post on Zulip Zesen Qian (Jul 21 2018 at 20:49):

RT, something like this in lean?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Zesen Qian (Jul 21 2018 at 21:05):

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

view this post on Zulip Simon Hudon (Jul 21 2018 at 21:05):

You write @[derive has_reflect] above your type definition

view this post on Zulip Mario Carneiro (Jul 21 2018 at 21:06):

I meant write a derive handler

view this post on Zulip Zesen Qian (Jul 21 2018 at 21:07):

@Simon Hudon very cool, thanks.

view this post on Zulip Simon Hudon (Jul 21 2018 at 21:09):

You're welcome

view this post on Zulip 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