tactic type class instance

Stream: general

[petercommand]

meta def opt_fst (a: tactic unit) (b: tactic unit) : tactic unit := (a >> b) <|> b

I am trying to define a tactic combinator, but it seems that I cannot use it like this:

opt_fst { symmetry } { symmetry }

and I am getting errors like

failed to synthesize type class instance for
|- has_emptyc (tactic unit)

Am I doing something wrong here?

[petercommand]

I want the tactic to accept begin...end blocks or {...} blocks

[Sebastian Ullrich]

You'll want your parameters to have type itactic (for "interactive tactic"). Try searching for itactic in core or mathlib for examples.

[Rob Lewis]

meta def tactic.interactive.opt_fst (a: tactic.interactive.itactic) (b: tactic.interactive.itactic) : tactic unit := (a >> b) <|> b

[petercommand]

Isn't tactic.interactive.itactic defined as tactic unit?

[Sebastian Ullrich]

Yes, but it's special-cased in the tactic block parser

[petercommand]

Ah

[petercommand]

Hmm..I am still getting the same error

[Gabriel Ebner]

You need to call it inside begin..end: begin opt_fst {} {} end

[petercommand]

do I have to prefix the name of the tactic with tactic.interactive.?

[Gabriel Ebner]

No.

[Sebastian Ullrich]

(if you're in tactic.interactive, which your definition should be)

[petercommand]

after changing the name of the tactic, it worked..

[Rob Lewis]

The tactic should be named tactic.interactive.whatever. You don't need to write the tactic.interactive part when you use it.

[petercommand]

The tactic should be named tactic.interactive.whatever. You don't need to write the tactic.interactive part when you use it.

Hmm..seems that this is also hardcoded

[petercommand]

Thanks!