Zulip Chat Archive

Stream: general

Topic: implicit variables


view this post on Zulip 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?

view this post on Zulip Simon Hudon (Jul 03 2019 at 18:17):

I'd make them implicit too

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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