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.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.LocalDecl.ldecl index fvarId userName type value nondep kind).ppAsBinder = none

@[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.

Equations

• fvarId.ppAsBinder = do let __do_lift ← fvarId.getDecl pure __do_lift.ppAsBinder