composing tactics

Stream: general

[Andrew Ashworth]

Suppose I prove a goal using by repeat {constructor}. What is the syntax for creating a new def of type tactic unit that does the same thing? Do I have to drop down into using the non-interactive tactics?

[Andrew Ashworth]

I guess handling the context and goals explicitly in a do block isn't so bad, but I was wondering if this is the correct way to do it

[Andrew Ashworth]

ahh, figured it out. it's just interactive.repeat interactive.constructor. I didn't know about the itactic type

[Gabriel Ebner]

1) Go to the definition of tactic.interactive.repeatand look how its defined. I don't know if we have any documentation on how to write interactive tactics beyond the ICFP paper. Short version: when you use begin foo bar end, lean looks for a definition named tactic.interactive.foo. The type of the arguments of tactic.interactive.foo determine how the arguments to the tactic are parsed. For example, itactic tells lean to parse a tactic block in curly braces.

[Gabriel Ebner]

2) You can use `[repeat {constructor}] to use interactive tactic syntax outside of begin-end blocks.