Expaning a macro into a macro

Stream: lean4

[Adam Topaz]

I'm trying to figure out how to define a macro that expands into a macro. Consider, for example,

macro "foo" t:str : command => `(macro $t : term => `(0))

I would like the command foo "test" to give a macro test that expands to 0 : Nat. I can't seem to figure out how to accomplish this. What am I missing here?

[Mac]

You are doing it right. You just need to tell Lean that t is a string literal.

macro "foo" t:str : command => `(macro $t:str : term => `(0))
foo "test"
#eval test -- 0

[Adam Topaz]

Ah! Thank you!