Explicit hypothesis vs implication hypothesis convention

Stream: maths

[Mohamed Al-Fahim]

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]

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]

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]

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

[Johan Commelin]

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

[Mohamed Al-Fahim]

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

[Kenny Lau]

Yes.

[Mohamed Al-Fahim]

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.

[Kenny Lau]

Go ahead.

[Mohamed Al-Fahim]

https://github.com/leanprover-community/leanprover-community.github.io/pull/154