unsafe def
Lean.PrettyPrinter.runForNodeKind
{α : Type}
(attr : Lean.KeyedDeclsAttribute α)
(k : Lean.SyntaxNodeKind)
(interp : Lean.ParserDescr → Lean.CoreM α)
:
Equations
- Lean.PrettyPrinter.runForNodeKind attr k interp = do let a ← Lean.getEnv match Lean.KeyedDeclsAttribute.getValues attr a k with | p :: x => pure p | x => do let info ← Lean.getConstInfo k if (Lean.Expr.isConstOf (Lean.ConstantInfo.type info) `Lean.ParserDescr || Lean.Expr.isConstOf (Lean.ConstantInfo.type info) `Lean.TrailingParserDescr) = true then do let d ← Lean.evalConst Lean.ParserDescr k interp d else Lean.throwError (Lean.toMessageData "no declaration of attribute [" ++ Lean.toMessageData attr.defn.name ++ Lean.toMessageData "] found for '" ++ Lean.toMessageData k ++ Lean.toMessageData "'")