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.{.