Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-01 14:36
bc5f69ee
View on Github →
doc(Tactic/HelpCmd): fix typo (option -> attribute) (
#15307
)
Estimated changes
Modified
Mathlib/Tactic/HelpCmd.lean