Expected Term Error

Stream: new members

[Joseph O]

With this macro, i get the error expected term

syntax ident ident "=" term ";" : command

macro_rules
  | `($ty:ident $name:ident = $v;) =>
    `(let $name:ident : $ty:ident := $v)

but when I make $v into $v:term, it gives a weirder error. Any ideas?

[Joseph O]

And this is Lean 4 fyi

[Joseph O]

I tried changing command into term, but that didn't help

[Joseph O]

Bumping