Matchin on syntax with group

Stream: lean4

[Joachim Breitner]

I have

syntax (name := find_theorems)
  withPosition("#find_theorems" (colGt (strLit <|> ident <|> term:max))+) : command

and it works, and I want to extend it to

syntax (name := find_theorems)
  withPosition("#find_theorems" (colGt (strLit <|> ident <|> ("⊢ " term:max) <|> term:max))+) : command

This is accepted, but if I then use

#find_theorems ⊢ (tsum _ = _) (_ * _ ^ _)

I get

elaboration function for 'group' has not been implemented
  [Error pretty printing syntax: unknown constant 'group'. Falling back to raw printer.]
  (group "⊢" (Term.paren "(" («term_=_» (Term.app `tsum [(Term.hole "_")]) "=" (Term.hole "_")) ")"))

I am parsing the argument list like this so far:

    for s in stx[1].getArgs do
      match s with
      | `($ss:str) => do
        let str := Lean.TSyntax.getString ss
        name_pats := name_pats.push str
      | `($i:ident) => do
        let n := Lean.TSyntax.getId i
        unless (← getEnv).contains n do
          throwErrorAt i "Name {n} not in scope"
        idents := idents.push n
      | `(group "⊢" $st:term) => do
        let t ← Lean.Elab.Term.elabTerm st none
        terms := terms.push (true, t)
      | _ => do
        let t ← Lean.Elab.Term.elabTerm s none
        terms := terms.push (false, t)

where the second-to-last clause is new. I found in the docs of <|> that it adds a group node if necessary, but I am unsure how to match it, or if I am approaching this the wrong way.

[Joachim Breitner]

I think I figured it out.