HepLean Documentation
Lean
.
PrettyPrinter
.
Basic
Search
Google site search
return to top
source
Imports
Lean.KeyedDeclsAttribute
Imported by
Lean
.
PrettyPrinter
.
backtrackExceptionId
Lean
.
PrettyPrinter
.
runForNodeKind
source
opaque
Lean
.
PrettyPrinter
.
backtrackExceptionId
:
Lean.InternalExceptionId
source
unsafe def
Lean
.
PrettyPrinter
.
runForNodeKind
{α :
Type
}
(attr :
Lean.KeyedDeclsAttribute
α
)
(k :
Lean.SyntaxNodeKind
)
(interp :
Lean.ParserDescr
→
Lean.CoreM
α
)
:
Lean.CoreM
α
Instances For