Topic: bounded exists
Patrick Massot (Feb 20 2019 at 22:31):
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 (Feb 20 2019 at 22:34):
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 (Feb 20 2019 at 22:35):
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 (Feb 21 2019 at 00:54):
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 (Feb 21 2019 at 08:10):
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.
Last updated: May 14 2021 at 11:10 UTC