bounded exists

Stream: general

[Patrick Massot]

The fact that ∃ δ > 0, ... parses as ∃ (δ :ℝ) (H : δ > 0), ... rather than ∃ δ : ℝ, δ > 0 ∧ ... is really a pain for teaching. @Sebastian Ullrich do you think the Lean 4 parser will allow us to choose here? Or even better, is it already possible in Lean 3?

[Patrick Massot]

As @Jeremy Avigad predicted in Amsterdam, hiding from students the fact that Lean uses non-set theoretic foundations is surprisingly easy. Until you get to bounded existential like ∃ δ > 0. I couldn't find any convincing lie to interpret this ∃ H : δ > 0.

[Patrick Massot]

By the way, will the new parser be accompanied by a more customizable pretty printer? It would be even better to also keep ∀ ε > 0 like this in the Lean messages view.

[Jeremy Avigad]

By way of clarification, my observation was not so much that we can hide the foundation from students, but, rather, that we don't have to apologize for it. Informal mathematics is what it is, and we can explain it to students and they can learn how to read and write ordinary proofs. Translating informal mathematics to any formal language -- set theory, type theory, or anything else -- requires adopting a rigid syntax. If we get over the idea that we have to pretend that informal proofs and formal proofs are the same thing, students have no problem learning the formal rules and understanding how they relate to the informal proof patterns. Being honest and straightforward is the best policy.

[Sebastian Ullrich]

do you think the Lean 4 parser will allow us to choose here? Or even better, is it already possible in Lean 3?
By the way, will the new parser be accompanied by a more customizable pretty printer?

Yes. No. Yes.