def Lean.LocalDecl.ppAsBinder : LocalDecl → Option MessageData

Pretty-prints a local declaration and its type as a binder, using the appropriate brackets given its BinderInfo. Example output: {α : Type}.

Returns none for let decls.

@[inline]

def Lean.FVarId.ppAsBinder (fvarId : FVarId) : MetaM (Option MessageData)

Pretty-prints a free variable and its type as a binder, using the appropriate brackets given its BinderInfo. Example output: {α : Type}.

Returns none for let decls.