List of tactics

Stream: lean4

[Leni Aniva]

Is there a function for querying the list of available tactics?

[Damiano Testa]

#help tactic should work.

[Leni Aniva]

Damiano Testa said:

#help tactic should work.

Is there a way to execute this in a CoreM monad?

[Damiano Testa]

You can look at the implementation, but the command itself does read the information off the environment, so I'm going to go with "yes"...