Zulip Chat Archive
Stream: mathlib4
Topic: data.set.pairwise.basic
Newell Jensen (Mar 27 2023 at 00:26):
When looking for an unported file that had many dependents I noticed that data.set.pairwise.basic was still available. On further inspection though I noticed that this file in mathlib3 mentions that it is synced with a file in mathlib4 but mathlib4 doesn't have a Pairwise folder and seems the contents (or at least a portion of them as I didn't inspect the entire file) are actually in mathlib4 in the file Data.Set.Pairwise.lean.
Something seems off (or I am misunderstanding something). Is this file supposed to still be in the unported files in the port-dashboard?
Yaël Dillies (Mar 27 2023 at 00:28):
Please don't touch :smile: It comes from a recent split.
Eric Wieser (Mar 27 2023 at 00:29):
This file was created in #17880, and will need handling as a forward-port
Yaël Dillies (Mar 27 2023 at 01:22):
Here's the forward port: !4#3117
Eric Wieser (Mar 27 2023 at 01:23):
I'll review that tomorrow
Eric Wieser (Mar 27 2023 at 10:12):
We need to forward-port #18636 first
Last updated: Dec 20 2023 at 11:08 UTC