def
Lean.PrettyPrinter.Delaborator.withOverApp
(arity : Nat)
(x : 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)

## Equations

- One or more equations did not get rendered due to their size.

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

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, #[])