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

Estimated changes