## Stream: maths

### Topic: Explicit hypothesis vs implication hypothesis convention

#### Mohamed Al-Fahim (Dec 29 2020 at 03:18):

Is there a convention for when to put the hypothesis to the left of the colon rather than in an implication?
For instance,

example (n : ℝ) (h : n > 1) : n > 0 := by linarith


rather than

example (n : ℝ) : (n > 1) → (n > 0) := λ h, (by linarith)


#### Bryan Gin-ge Chen (Dec 29 2020 at 05:41):

Between your two examples, I think we generally prefer the former, since it removes the need for the lambda after the :=. So I generally put as many hypotheses to the left of the colon as possible. Sometimes you have to leave some implications or foralls to the right of the colon, especially when using the equation compiler or if the proof uses tactic#induction.

#### Mohamed Al-Fahim (Dec 29 2020 at 07:39):

Bryan Gin-ge Chen said:

Between your two examples, I think we generally prefer the former, since it removes the need for the lambda after the :=. So I generally put as many hypotheses to the left of the colon as possible. Sometimes you have to leave some implications or foralls to the right of the colon, especially when using the equation compiler or if the proof uses tactic#induction.

Would the former be preferred even if the proof didn't contain a lambda, but rather a begin-end block?

#### Johan Commelin (Dec 29 2020 at 07:52):

if the begin .. end-block starts with intros you might as well put those assumptions left of the colon.

#### Johan Commelin (Dec 29 2020 at 07:53):

It's mostly just about which version uses the least amount of characters to type...

#### Mohamed Al-Fahim (Dec 29 2020 at 07:55):

So generally speaking, it is better to put hypotheses to the left of the colon as much as possible.

Yes.

#### Mohamed Al-Fahim (Dec 29 2020 at 08:03):

I see. I can make a pull request to add this convention to Style Guidelines https://leanprover-community.github.io/contribute/style.html, since it seems useful.