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)
Instances For

    Inner loop of withOverApp.

    Instances For

      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.

      Instances For