running an existing parser

Stream: Is there code for X?

[Joachim Breitner]

I have a String, a syntactic category, and I want to get the Syntax out. How would I do that? I tried the following:

import Lean.Meta
import Mathlib.Tactic.RunCmd

open Lean Core Meta Elab Term Command

run_cmd liftTermElabM do
  let x := Parser.runParserCategory (← getEnv) ``Lean.Parser.Tactic.Conv.arg "arg 1"
  IO.println x

but I get

error: <input>:1:0: unknown parser category 'Lean.Parser.Tactic.Conv.arg'

So somehow the parser environment isn’t set up properly, I assume?

(Using Lean.Parser.Tactic.Conv.arg here is just an arbitrary example)

Maybe I can use that ParserDescr directly?

[Joachim Breitner]

I think I figured it out; I need to use declare_syntax_cat it seems