## Stream: general

### Topic: implicit variables

#### Kevin Buzzard (Jul 03 2019 at 18:04):

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 (Jul 03 2019 at 18:17):

I'd make them implicit too

#### Mario Carneiro (Jul 03 2019 at 18:27):

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

#### Mario Carneiro (Jul 03 2019 at 18:27):

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

#### Mario Carneiro (Jul 03 2019 at 18:28):

If the axiom is restated it can be implicit as normal

Last updated: May 14 2021 at 04:22 UTC