Mathlib Changelog
v4
Changelog
About
Github
Def
Tactic.Alias.Target.toString
Modification history
2023-08-23 04:19
Mathlib/Tactic/Alias.lean
feat: patch for new alias command (#6172)
Deleted
Tactic.Alias.Target.toString
View on Github →
2022-11-14 23:06
Mathlib/Tactic/Alias.lean
feat: add doc strings in alias command (#598) …
Added
Tactic.Alias.Target.toString
View on Github →