Zulip Chat Archive

This PR is a possible improvement to the Lean pretty printer. I'm not sure if it will be merged, but it seems like it's worth thinking about. The PR came from some experimentation after a question by @Dan Velleman in this topic about Lean 4's pretty printing rules for foralls.

The basic motivation is that it is occasionally (and pedagogically) surprising when a non-dependent forall switches from being pretty printed with the forall notation to using the function arrow. Foralls are fairly special as far as pi types go. Recall that if A : Sort u and B : A → Sort v then

Π (a : A), B a : Sort (imax u v)

If v is 0 then this is ∀ (a : A), B a : Prop, but if v is nonzero then this is Π (a : A), B a : Sort (max u v) (definitely not a Prop).

The current pretty printing rules are that if B is non-dependent (say B : Sort v), then Π (a : A), B pretty prints as A → B in both cases. An observation is that the "surprising" case is when v is zero and u is nonzero, since A → B : Prop but A is not a proposition.

What this PR does is cause the pretty printer to show ∀ (_ : A), B in this case, to let the user know that this is a pi type in Prop with a non-Prop binder. The _ indicates that this is a non-dependent forall, so pretty printing this way provides strictly more information to the user than before. Prop-to-prop implications still pretty print as A → B.

Furthermore, since it was simpler to implement this way, the PR has the pretty printer replace non-dependent binders in pi types with _ in general, for instance Π {_ : ℕ}, ℤ rather than Π {n : ℕ}, ℤ (but still ℕ → ℤ rather than Π (n : ℕ), ℤ for non-dependent explicit binders). It seems to be more useful to know that a pi is non-dependent than to know the name of the binder.