leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
211 stars 50 forks source link

metam: use `isImplementationDetail` instead of `isAuxDecl` #76

Closed JLimperg closed 1 year ago

JLimperg commented 1 year ago

(Note to self:) when we iterate over a local context, it does not suffice any more to exclude hypotheses for which isAuxDecl is true; we have to check isImplementationDetail.