commands elaborating ... commands

Stream: metaprogramming / tactics

[Frederic Peschanski]

I am trying to implement new commands but in the metaprogramming lean4 book most (if not all ?) examples of elaborations of commands only yield logInfo messages.
In my case, I would like to make various declarations (e.g. generated defs, defining types and functions, etc.) but I would also like to call other commands.
As a simple example (of course trivial, just not for me), I would like to create a synonymous for namespace.

E.g. instead of writing :

namespace MyNS
...
end MyNS

I would like to write :

spacename MyNS
...
end MyNS

Of course it's silly but still, I would be happy if you can point me in the right direction.
As a side note I would prefer to be directly at the CommandElabM level.

[Kyle Miller]

In that case you can make a macro:

macro "spacename" n:ident : command => `(command| namespace $n)

[Kyle Miller]

Here's an elaborator:

open Lean Elab Command

elab "spacename" n:ident : command => do
  let cmd ← `(command| namespace $n)
  elabCommand cmd

[Frederic Peschanski]

Kyle Miller said:

Here's an elaborator: ...

Thank you very much ! (I need to learn more about the quotations ...)