Commit 2023-04-28 23:45 394e6b88

View on Github →

feat: make alias compile code when possible (#3719)

Estimated changes

Modified Mathlib/Tactic/Alias.lean

Modified test/Alias.lean

added def Alias.baz

added def Alias.foo