def testExternCmd : Lean.ParserDescr

Equations

• testExternCmd = Lean.ParserDescr.node `testExternCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "test_extern ") (Lean.ParserDescr.cat `term 0))

unsafe def elabTestExtern : Lean.Elab.Command.CommandElab