Printing the binder in Exists

Stream: lean4

[Kyle Miller]

Jovan Gerbscheid said:

It would be nice if ∃ and ∀ printed the same. Currently, only ∀shows the binder types (which can be turned off using pp.piBinderTypes).

This is something I think about trying to solve periodically.

Here's an overview of the situation:

• The forall notation is from a raw pi type. There's a delaborator responsible for pretty printing, since there are a number of calculations it needs to do (e.g. to decide between forall and (x : a) -> b x notation).
• The exists notation uses an app unexpander.
  • App unexpanders are syntax transformers that are applied inside the app delaborator. The sequence goes: delaborate the function and arguments for an application (skipping implicit arguments), create the application, then try applying unexpanders if the function is a constant.
  • The Exists unexpander sees an expression of the form Exists fun ... => ..., where fun ... => ... is a predicate.
  • Depending on the value of pp.funBinderTypes, this fun might or might not have a binder type. If it doesn't, the unexpander doesn't have access to the existential's domain at all. Unexpanders do not have any access to the underlying expression, just the pretty printed results.
  • Even if an unexpander had a way to re-pretty-print an argument with additional options, it would be best to avoid re-pretty-printing. Delaboration doesn't have any memoization, which would lead to O(n^2) pretty printing calls for an exists chain of length n.

A couple potential directions I've thought about:

1. Add a system where you can tag a specific constant with pretty printer option rules. For example, on Exists we could add the rule "set pp.funBinderTypes on argument 1". This way the unexpander has the domain to work with. Downside: this will always show the existential's domain unless the system can also be made conditional on option(s).
2. Switch to using a delaborator. This gives up on a general solution, but it does address the pain point with Exists. I think Mathlib tends to use notation3 instead of trying to write app unexpanders for notations with binders.

A virtue of app unexpanders is that they let you define how to pretty print notation without needing to import anything in Lean.

For Exists though, in core it's possible to create a "builtin" delaborator. These can be defined after the prelude, but are already pre-loaded in the prelude. That means you'd still see Exists pretty printed even without importing anything.

[Aaron Liu]

Jovan Gerbscheid said:

It would be nice if ∃ and ∀ printed the same. Currently, only ∀shows the binder types (which can be turned off using pp.piBinderTypes).

You can turn on binder types for ∃ with pp.funBinderTypes

[Jovan Gerbscheid]

Here's another related issue.

If I click on ∃ a > 4, a = a in the infoview, it shows me that the term is secretly @Exists ℕ fun a => a > 4 ∧ a = a, which is nice to know.

But if I click on ∀ a > 4, a = a, it still shows me ∀ a > 4, a = a, and I have no way to see what is actually there.

[Robin Arnez]

Yeah I guess that's especially bad for not allowing you to investigate the a > 4 expression itself and e.g. look at the instance. The solution would be to prevent the delaborator that turns ∀ a, a > 4 → a = a into ∀ a > 4, a = a when pp.explicit is true (which is used among others when you hover over an expression). This is a mathlib thing though, so we can fix it directly in mathlib.

[Aaron Liu]

probably docs#PiNotation.delabPi