Commit 2022-11-24 14:35 20713f84

fix: let toAdditive handle more auxiliary declarations (#699)

• This PR will correctly deal with names starting with env.mainModule ++ `_auxLemma (generated by simp)
• Also add a test for this case (reported on Zulip)
• Also correctly deal with equation lemmas, which are have mkPrivateName env pre as prefix, instead of pre. It fixes both of the following issues:
  • Previously this would sometimes not translate the equation lemmas, since the naming heuristic didn't change their name
  • If it would translate a lemma, it would not apply it, since it wasn't additive to the translations dictionary.