Instances For
Instances For
Instances For
Instances For
def
Lean.PrettyPrinter.ppExprWithInfos
(e : Lean.Expr)
(optsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅)
(delab : optParam Lean.PrettyPrinter.Delaborator.Delab Lean.PrettyPrinter.Delaborator.delab)
:
Return a fmt
representing pretty-printed e
together with a map from tags in fmt
to Elab.Info
nodes produced by the delaborator at various subexpressions of e
.
Instances For
@[export lean_pp_expr]
def
Lean.PrettyPrinter.ppExprLegacy
(env : Lean.Environment)
(mctx : Lean.MetavarContext)
(lctx : Lean.LocalContext)
(opts : Lean.Options)
(e : Lean.Expr)
:
Instances For
Instances For
Instances For
Pretty-prints a declaration c
as c.{
.