def Lean.PrettyPrinter.Delaborator.withOverApp (arity : Nat) (x : Lean.PrettyPrinter.Delaborator.Delab) : Lean.PrettyPrinter.Delaborator.Delab

This is similar to withAppFnArgs but it handles construction of an "over-application". For example, suppose we want to implement a delaborator for applications of f : Foo A → A like f x as F[x], but because A is a type variable we might encounter a term of the form @f (A → B) x y which has an additional argument y.

Most of the built in delaborators will deliberately fail on such an example, resulting in delaborated syntax f x y, but this combinator can be used if we want to display F[x] y instead.

• arity: the expected number of arguments to f. The combinator will fail if fewer than this number of arguments are passed
• x: constructs data corresponding to the main application (f x in the example)

def Lean.PrettyPrinter.Delaborator.withOverApp.loop (arity : Nat) (x : Lean.PrettyPrinter.Delaborator.Delab) (kinds : Array Lean.PrettyPrinter.Delaborator.ParamKind) : Nat → Lean.PrettyPrinter.Delaborator.DelabM (Lean.Term × Array Lean.Term)

Inner loop of withOverApp.

Equations

• One or more equations did not get rendered due to their size.
• Lean.PrettyPrinter.Delaborator.withOverApp.loop arity x kinds 0 = do let __do_lift ← x pure (__do_lift, #[])

def Lean.ppConst (e : Lean.Expr) : Lean.MessageData

Pretty print a const expression using delabConst and generate terminfo. This function avoids inserting @ if the constant is for a function whose first argument is implicit, which is what the default toMessageData for Expr does. Panics if e is not a constant.