has_reflect

Stream: mathlib4

[Jireh Loreaux]

I was about to start porting data.num.basic, not because it's important, but just to get my hands dirty porting. But immediately there is a deriving has_reflect, and I don't know what the Lean 4 analogue of docs#has_reflect is. Is it by chance docs4#Lean.ToExpr?

[Jireh Loreaux]

If I use that instead I get the error

-- default handlers have not been implemented yet, class: 'Lean.ToExpr' types: [PosNum]

which I suppose means there is no standard way to create a ToExpr instance via deriving.

[Alex J. Best]

I think thats correct yes, I'd say the has reflect instance for num probably isn't used much anyway, so its ok to ignore for now.

[Eric Wieser]

This feels like it should be an easy default handler to write; all you have to do is turn num.bit0 x into `(num.bit0 %`(x)) etc; while writing the general metaprogram might be annoying right now, writing the special case for just num should be trivial.

[Eric Wieser]

This feels like it should be an easy default handler to write; all you have to do is turn num.bit0 x into `(num.bit0 %`(x)) etc; while writing the general metaprogram might be annoying right now, writing the special case for just num should be trivial.

[Alex J. Best]

Sure but if the general case will come eventually and this will never be used what is the point of adding this one special case now?

[Jireh Loreaux]

@Eric Wieser, I'll have a PR in about 20 minutes or so. If you want to add it for PosNum I can try to do the rest based on your example.

[Mario Carneiro]

I don't think that Lean.ToExpr instances are being used at all currently outside the few examples in core. Let's wait until we have a clear sense of what it needs to do, and then implement a derive handler for it. I might add a dummy Lean.ToExpr derive handler which just does nothing so that people don't have to worry about it

[Alex J. Best]

It's used in quote4 a bit I think, not sure how essentially but it makes some sense that it would be helpful there at least

[Mario Carneiro]

are you sure? I don't see any examples of using ToExpr on arbitrary user-provided types in quote4

[Alex J. Best]

Ah I see, you're not saying that ToExpr isn't used, just that instances do nothing for now? I guess that could be true

[Mario Carneiro]

The use of ToExpr inside quote4 is all for a closed class of types, for which things like the fact that it only works on types in Type is not a problem

[Mario Carneiro]

for the most part, I find that quote4 itself replaces most uses of has_reflect

[Mario Carneiro]

but we could have a Qq-powered ToExprQ typeclass that has a better type signature