Documentation

Std.Lean.Delaborator

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.

Inner loop of withOverApp.

Equations