implicit variables

Stream: general

[Kevin Buzzard]

Recently Mario told me the algorithm for which variables should be implicit. So how come

partial_order.le_antisymm : ∀ {α : Type u_1} [c : partial_order α] (a b : α), a ≤ b → b ≤ a → a = b

? Shouldn't a and b be implicit here because you can read them off from e.g. a ≤ b?

[Simon Hudon]

I'd make them implicit too

[Mario Carneiro]

They are explicit because lean has a bug which makes structure projections not actually work with implicit args

[Mario Carneiro]

They could also be semi-implicit {{a b: A}}, but implicit is just inviting confusion when it doesn't work

[Mario Carneiro]

If the axiom is restated it can be implicit as normal