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
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
Most of the built in delaborators will deliberately fail on such an example, resulting in
f x y, but this combinator can be used if we want to display
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 xin the example)
Inner loop of
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
e is not a constant.