Commit 2022-10-22 01:52 f493ef4c

View on Github →

feat: track "synthetic" and "dubious" #align (#488) Companion PR to leanprover-community/mathport#187

Estimated changes

Modified Mathlib/Mathport/Rename.lean

added structure Mathlib.Prelude.Rename.NameEntry

added def Mathlib.Prelude.Rename.RenameMap.find?

added def Mathlib.Prelude.Rename.RenameMap.insert

deleted def Mathlib.Prelude.Rename.RenameMap.insertPair

added structure Mathlib.Prelude.Rename.RenameMap

modified def Mathlib.Prelude.Rename.addNameAlignment

Modified Mathlib/Mathport/Syntax.lean