Zulip Chat Archive

Stream: general

Topic: obtain style


view this post on Zulip 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.

view this post on Zulip 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