Def Lean.Meta.unfoldAuxLemmas

Modification history

2026-01-09 10:48
Mathlib/Lean/Name.lean
fix(translate): don't unfold aux lemmas, but translate them (#33603) …
Deleted Lean.Meta.unfoldAuxLemmasView on Github →
2024-07-15 23:26
Mathlib/Lean/Name.lean
feat(to_additive): unfold lemmas generated by `simp` (#14628) …
Added Lean.Meta.unfoldAuxLemmasView on Github →