Gravifer

import Lean

open Lean

deriving instance Repr for ParserDescr

unsafe def getParserDescrUnsafe (name : Name) : CoreM (Option ParserDescr) := do
  let info ← getConstInfo name
  if info.type.isConstOf ``ParserDescr || info.type.isConstOf ``TrailingParserDescr then
    return some (← evalConst ParserDescr info.name)