macro_rules with equation symbol

Stream: lean4

[Ira Fesefeldt]

I have a syntax category in which I would like to use equality symbols. For some reason, however, macro_rules does not think I should use them. Instead I get the error unexpected token ']'; expected '='. Why does this happen and how to solve this?

MWE:

declare_syntax_cat eq

syntax term " = " term : eq
syntax "[eq|" eq "]" : term

def my_eq {α : Type} (a b : α) : Prop := sorry

macro_rules
  | `([eq| $a:term = $b:term]) => `(my_eq $a $b)

[Eric Wieser]

The issue is that the term on the LHS is consuming the =, because that already is valid as a term

[Eric Wieser]

(Separately, you probably want `(term| [eq| $a:term = $b:term]) to remind lean what category you are trying to match)

[Ira Fesefeldt]

Ah. I see. Thanks for the explanation!

[Sebastian Ullrich]

And the way to solve that is to increase the precedence, syntax term:51 " = " term:51 : eq

[Sebastian Ullrich]

@Eric Wieser term is the default category