Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC