Def Tactic.Alias.aliasIff

Modification history

2023-08-23 04:19
Mathlib/Tactic/Alias.lean
feat: patch for new alias command (#6172)
Deleted Tactic.Alias.aliasIffView on Github →
2022-11-14 23:06
Mathlib/Tactic/Alias.lean
feat: add doc strings in alias command (#598) …
Modified Tactic.Alias.aliasIffView on Github →
2022-09-15 13:26
Mathlib/Tactic/Alias.lean
fix: various bors issues (#413)
Modified Tactic.Alias.aliasIffView on Github →
2022-09-15 12:35
Mathlib/Tactic/Alias.lean
feat: better info tracking in `alias` (#408) …
Modified Tactic.Alias.aliasIffView on Github →
2022-06-30 08:11
Mathlib/Tactic/Alias.lean
feat: port the 'alias' command (#293) …
Added Tactic.Alias.aliasIffView on Github →