Commit 2022-06-30 08:11 60d54415

View on Github →

feat: port the 'alias' command (#293) Compare to https://github.com/leanprover-community/mathlib/blob/07c83c81c0016c1ac08e8c9c3f1260c2f4c6ac7f/src/tactic/alias.lean The mkIffMpApp and aliasIff functions are direct translations of the mathlib3 versions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Alias.lean

added def Tactic.Alias.aliasIff

added def Tactic.Alias.appendNamespace

added def Tactic.Alias.elabAlias

added def Tactic.Alias.elabAliasLR

added def Tactic.Alias.elabAliasLRDots

added def Tactic.Alias.mkIffMpApp

added theorem alias1

added theorem alias2

Created test/Alias.lean

added theorem Alias.A.a_iff_a_and_a

added theorem Alias.A.ab_iff_ba

added def Alias.A.bar

added theorem Alias.A.baz

added theorem Alias.A.foo