Def Tactic.Alias.elabAliasLRDots
Modification history
2023-08-23 04:19
Mathlib/Tactic/Alias.lean
feat: patch for new alias command (#6172)
Deleted Tactic.Alias.elabAliasLRDotsView on Github →2022-10-20 15:23
Mathlib/Tactic/Alias.lean
chore: update lean + std4 10-20 (#483)
Modified Tactic.Alias.elabAliasLRDotsView on Github →