Commit 2023-12-28 17:56 bf19b01f

View on Github →

chore: remove Name.isInternal' in favour of Name.isInternalDetail (#9196) We can remove Name.isInternal' as it exists in std as Name.isInternalDetail.

Estimated changes

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Name.isInternal'

Modified Mathlib/Lean/Name.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Tactic/ToAdditive.lean