metaprogramming: why must syntax and macro_rule disagree?

Stream: general

[Quinn]

inductive Foo where
| Bar (x : String) (y : Nat)

declare_syntax_cat fooing
syntax "bβ" term num : fooing

macro_rules
| `(β $a $b) => `(Foo.Bar $a $b)

#check β "x" 1

I can't figure out why when i change it to syntax "β" term num : fooing it doesn't work (says "unexpected token, expected term")

[Quinn]

here's the minimal reproducer of my actual problem

inductive Distribution where
  | Bernoulli (p : Float) : Distribution

inductive Command where
  | Sample (x : String) (d : Distribution) : Command

declare_syntax_cat dist
syntax "Bern(" term ")" : dist
declare_syntax_cat cmd
syntax term "~" dist : cmd

macro_rules
  | `($x ~ Bern($p)) => `(Command.Sample $x (Distribution.Bernoulli $p))

[Jannis Limperg]

Fixed:

inductive Distribution where
  | Bernoulli (p : Float) : Distribution

inductive Command where
  | Sample (x : String) (d : Distribution) : Command

declare_syntax_cat dist
syntax "Bern(" term ")" : dist
declare_syntax_cat cmd
syntax term "~" dist : cmd

macro_rules
  | `(cmd| $x:term ~ Bern($p)) => `(Command.Sample $x (Distribution.Bernoulli $p))

When you're not working with the default syntax category term, you must give the syntax category in the syntax quotation: cmd|. And then add type annotations to your variables until it works: $x:term.

[Quinn]

ok this is great, thanks!