Commit 2022-09-15 12:35 3ccef233

View on Github →

feat: better info tracking in alias (#408) This lets you hover over the identifiers in alias to see the types of things, and go to definition works.

Estimated changes

Modified Mathlib/Tactic/Alias.lean

modified def Tactic.Alias.aliasIff

modified def Tactic.Alias.elabAlias

modified def Tactic.Alias.elabAliasLR

modified def Tactic.Alias.elabAliasLRDots