## Stream: general

### 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 rcases/rintros/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