How does texpr parse numerals?

Stream: metaprogramming / tactics

[Bhavik Mehta]

section

open tactic
open interactive

meta def my_refine (q : parse types.texpr) : tactic unit :=
tactic.refine q

end

example : ℕ :=
begin
  refine 1,
end

example : ℕ :=
begin
  my_refine 1,
end

I'm not sure why the first example succeeds but the second doesn't!

[Mario Carneiro]

you didn't put my_refine in the tactic.interactive namespace, so it's parsing my_refine 1 as an application