Zulip Chat Archive

Stream: general

Topic: derive handlers


Simon Hudon (Aug 31 2018 at 20:56):

I'm writing a derive handler, and while testing it on my third example, I get the following error:

declaration contains macro with trust-level higher than the one allowed (possible solution: unfold macro, or increase trust-level)

But the term that my handler produces contains no macros that I can see (I'm using expr.fold to enumerate them). Has anyone seen this before?

Simon Hudon (Aug 31 2018 at 21:00):

Update: I checked a part of the derived term which produces perm_ac and ac_app

Simon Hudon (Aug 31 2018 at 21:22):

Update 2: I wrote a tactic expand_untrusted that takes care of those macros. It solves the problem. I'm surprised instance_derive_handler doesn't do that by default


Last updated: Dec 20 2023 at 11:08 UTC