tactic parser

Stream: metaprogramming / tactics

[Heather Macbeth]

Simple question, but how do I write a tactic taking two arguments?

import tactic

namespace tactic.interactive

setup_tactic_parser

meta def foo (p : parse (parser.pexpr 0)) : tactic unit :=
do trace p

meta def foo₂ (p q : parse (parser.pexpr 0)) : tactic unit :=
do trace p,
   trace q

end tactic.interactive

example : true :=
begin
  foo 3, -- fine
  foo₂ 3 4, -- error "expression expected"
end

[Kyle Miller]

If I'm understanding what's going on, it's parsing 3 4 as one expression (a function application with one argument).

[Kyle Miller]

If you have it use the default highest precedence, it works

import tactic

namespace tactic.interactive

setup_tactic_parser

meta def foo (p : parse (parser.pexpr 0)) : tactic unit :=
do trace p

meta def foo₂ (p q : parse parser.pexpr) : tactic unit :=
do trace p,
   trace q

end tactic.interactive

example : true :=
begin
  foo (3 + 2) 4, -- fine
  foo₂ (3 + 2) 4, -- fine
end

[Heather Macbeth]

Thanks!