Commit 2022-11-14 23:06 4d10f38e
View on Github →feat: add doc strings in alias command (#598) Follows the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/1158f6d88df46d30c657ffce6bfdb9e9aceb4955/src/tactic/alias.lean#L85
feat: add doc strings in alias command (#598) Follows the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/1158f6d88df46d30c657ffce6bfdb9e9aceb4955/src/tactic/alias.lean#L85