Topic: obtain style
Patrick Massot (Sep 25 2020 at 09:21):
I have a style question. I see in Reid's PR:
obtain ⟨c, hc₁, hc₂⟩ : ∃ c : α, a < c ∧ c < b := dense h, which is the traditional way to use
obtain to make proofs more readable. Somewhat recently, Mario extend the parsing so that we can put type annotations in
obtain. Should we switch to
obtain ⟨c : α, hc₁ : a < c, hc₂ : c < b⟩ := dense h,? I don't have a strong opinion here. The first version is nice because the existential quantifier is explicit, the second version makes it clearer what we indeed obtain.
Johan Commelin (Sep 25 2020 at 09:23):
I think both are fine. Let's use seems reasonable at that point.
Last updated: May 12 2021 at 04:19 UTC