Skip to content

feat: port data.set.prod#978

Closed
Ruben-VandeVelde wants to merge 4 commits intomasterfrom
data.set.prod
Closed

feat: port data.set.prod#978
Ruben-VandeVelde wants to merge 4 commits intomasterfrom
data.set.prod

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

No description provided.

@Ruben-VandeVelde Ruben-VandeVelde added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 13, 2022
@Ruben-VandeVelde Ruben-VandeVelde marked this pull request as ready for review December 13, 2022 13:58
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 13, 2022
kim-em added a commit that referenced this pull request Dec 14, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 14, 2022

Sorry about the duplicated work, I didn't see this. I'm going to close this in favour of #1004, which is now hopefully done.

@kim-em kim-em closed this Dec 14, 2022
@int-y1 int-y1 deleted the data.set.prod branch April 16, 2023 18:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

mathlib-port This is a port of a theory file from mathlib. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants