How to match on `<|>` syntax?

Stream: lean4

[Hanting Zhang]

Hello, I'm having trouble trying to get the following example to work

import Lean

open Lean Elab Meta

declare_syntax_cat my_cat

syntax op := "+" <|> "-" <|> "*" <|> "/"
syntax op : my_cat

def elabMyCat : Syntax → MetaM Expr
  | `(my_cat| $o:op) =>
    match o with
    | `(op| +) => return mkStrLit "+"
    | `(op| -) => return mkStrLit "-"
    | `(op| *) => return mkStrLit "*"
    | `(op| /) => return mkStrLit "/"
    | _ => throwUnsupportedSyntax
  | _ => throwUnsupportedSyntax

elab "[my_cat| " e:my_cat "]" : term =>
  elabMyCat e

#eval [my_cat| - ]

At the bottom #eval, no matter what I do, it always returns "+" and doesn't seem to be matching with the cases I've defined in elabMyCat. What am I missing? Thanks!

[David Renshaw]

Maybe this is the same as the issue I hit recently? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/commandElab.20behaving.20weirdly/near/287328051

[David Renshaw]

maybe https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/commandElab.20behaving.20weirdly/near/287227944 is a better link

[Hanting Zhang]

Ah... I see. Well, I only have atoms here so I guess this is a bit awkward. I'll just write out all the cases then