mathlib

13d4fbee - feat(tactic/interactive_attr): `@[interactive]` attribute to export interactive tactics (#3698)

feat(tactic/interactive_attr): `@[interactive]` attribute to export interactive tactics (#3698) Allows one to write ```lean @[interactive] meta def my_tactic := ... ``` instead of ```lean meta def my_tactic := ... run_cmd add_interactive [``my_tactic] ```