order of arguments

Stream: new members

[Daan van Gent]

Why is the order of arguments in

theorem sup_le_sup_left (h₁ : a ≤ b) (c) : c ⊔ a ≤ c ⊔ b

hypothesis h first and element c second, while

lemma inf_le_inf_right (a : α) {b c : α} (h : b ≤ c) : b ⊓ a ≤ c ⊓ a

is the other way around?

[Eric Wieser]

To me those both look backwards!

[Eric Wieser]

docs#sup_le_sup_right and docs#inf_le_inf_left both look right to me, in contrast

[Daan van Gent]

I see no difference between those and mine. Both don't agree on the order of element vs hypothesis, or is there some logic I am missing?

[Andrew Yang]

The order of the hypothesis should match the order of appearances in the statement.

[Daan van Gent]

What does that mean? The hypothesis h₁ : a ≤ b appears nowhere in the statement c ⊔ a ≤ c ⊔ b

[Eric Wieser]

It's more of a heuristic than an algorithm. c ⊔ a ≤ c ⊔ b is natural to think of as a ≤ b with c on the left, so in the arguments c is on the left of the a ≤ b argument.

[Daan van Gent]

I see, thanks! That's not something I would have guessed. I expected something like data to take precedence over propositions.

[Yaël Dillies]

Actually you should expect the other way because proof arguments are (usually) not inferrable from the rewrite, while data arguments are.