Infinite recursing macro?

Stream: new members

[Joseph O]

Im using lean 4, and i have this macro. I am wondering why it is infinitely recursing:

inductive Nat' where
  | zero
  | succ : Nat' → Nat'
  deriving Repr

open Nat'

syntax (name := to_nat') "nat!" term : term
macro_rules (kind := to_nat')
  | `(nat! 0) => `(Nat'.zero)
  | `(nat! $n) => `(Nat'.succ $ nat!($n-1))

#eval let seven := nat! 7; seven
/- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) -/

[Yakov Pechersky]

Won't nat! 0 match both rules? And then nat!($n-1) gives nat!0 because 0 - 1 = 0?

[Joseph O]

Yes, but shouldn't it stop on the first rule?

[Mauricio Collares]

1-1 probably does not match 0 for macro expansion purposes

[Joseph O]

Then do you have an alternative solution?