Tactic taking a parameter

Stream: Is there code for X?

[Ryan Ziegler]

I want to create a tactic that takes a real number as a parameter. For simplicity, let's say I want my tactic to just be

use x
simp

I've been able to write

macro "tooeasy" : tactic => `(tactic| use 1)

and this works fine, but I can't figure out how to make 1 a parameter to tooeasy. I looked a bit at polyrith, and tried

elab "cooluse" ppSpace args:term,+ : tactic =>
  `(tactic|use args.getElems.toList)

but get the following error about my body:

has type
  TSyntax `tactic : Type
but is expected to have type
  Unit : Type

I'm unclear why it's expected to have Unit. Any pointers would be appreciated! Thanks!

[Kyle Miller]

The error is that you used elab instead of macro (elab means it has to be completely responsible for running the tactic, but a macro is a syntax replacement)

[Kyle Miller]

macro "cooluse" ppSpace args:term,+ : tactic =>
  `(tactic| (use $[$args],*
             simp))

[Kyle Miller]

The next error you would have seen is that you're not substituting in args -- you need $ antiquotations to do substitutions.