## 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: May 14 2021 at 02:15 UTC