Get all tactics in scope

Stream: Is there code for X?

[Riyaz Ahuja]

Is there any command or function that allows me to view a list of the names of all tactics that are currently in scope? Kind of how I can look at (<- getEnv).constants to see all my constantInfos, is there any easy way to view all the tactics, or even better, where they were defined (e.g. a DeclarationRange and ModuleName?)

[Jon Eugster]

https://github.com/leanprover-community/mathlib-manual/blob/main/Manual%2FTactics%2FAll.lean#L58

You could take inspiration here. Maybe even look inside allTacticDocs which should be in Lean core, but I forgot which namespace something you open with open Lean Doc Elab

[Floris van Doorn]

You can also see a list of all tactics using #help tactic. If you want a metaprogrammatic way, you can look at the implementation of the #help command. (requires Batteries)