PR !4#9605: feat(Data/Finset & List): Add Lemmas for Sort...

Stream: triage

[Random Issue Bot]

Today I chose PR 9605 for discussion!

feat(Data/Finset & List): Add Lemmas for Sorting and Filtering
Created by @Andy Jiang (@davikrehalt) on 2024-01-10
Labels: awaiting-author, please-adopt, merge-conflict, new-contributor, t-data

Is this PR still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

This PR seems to have been abandoned.

[Violeta Hernández]

I've salvaged some of the results in here in #18465 and #18466.