Macro defined recursively on Nat

Stream: lean4

[Adam Topaz]

I'm trying to make a macro that will expand [nary 3 | Nat] to Nat -> Nat -> Nat -> Nat (with the obvious generalization of 3 and Nat).
So far I have something silly like the following, which doesn't work (as indicated) when using numerals:

syntax "[nary " term " | " term "]" : term

macro_rules
| `([nary 0 | $t:term]) => `($t)
| `([nary (Nat.succ $s:num) | $t:term]) => `($t → [nary $s | $t])

#check [nary 0 | Nat] -- Nat
#check [nary (Nat.succ 0) | Nat] -- Nat → Nat
#check [nary 1 | Nat] -- Fails: "elaboration function for ... has not been implemented"

Is there a way to accomplish this with macros, or do I need to do something more complicated? What am I missing?

[Hanting Zhang]

The following works:

syntax "[nary " term " | " term "]" : term

macro_rules
| `([nary $nat:num | $t:term]) => do
  let rec loop (n : ℕ) : MacroM (TSyntax `term) :=
    match n with
    | 0 => `($t)
    | n + 1 => do `($t → $(← loop n))
  loop nat.getNat

[Adam Topaz]

Thanks!

[Hanting Zhang]

Ah but if you want terms in general that evaluate into Nats, then the MacroM monad probably isn't strong enough -- you would need like TermElabM that can reduce and compute expressions for you

[Adam Topaz]

No, this is actually perfectly fine for what I was trying to do.