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

Equations

• One or more equations did not get rendered due to their size.