Zulip Chat Archive

Stream: general

Topic: Implicit pairwise arguments


Yaël Dillies (Dec 11 2021 at 17:05):

I'm changing docs#set.pairwise from ∀ x ∈ s, ∀ y ∈ s, x ≠ y → r x y to ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y. Should I do the same to docs#pairwise?

Mario Carneiro (Dec 12 2021 at 22:42):

There is no analogue of that change for docs#pairwise, since there are no membership assumptions in that case

Yaël Dillies (Dec 12 2021 at 22:48):

I don't know what you want to call it, if not "analog", but here's the change I want to make:

  • Currently: ∀ i j, i ≠ j → r i j
  • What I want: ∀ ⦃i j⦄, i ≠ j → r i j

Eric Wieser (Dec 12 2021 at 22:50):

I'd caution against changing both in the same PR


Last updated: Dec 20 2023 at 11:08 UTC