diff vs. sdiff

Stream: general

[Michael Stoll]

Is there a deeper reason why set difference is diff (in lemma names), but finset difference is sdiff?

[Yaël Dillies]

I guess people didn't want to call it "set set difference". But really we should align the names.

[Michael Stoll]

More generally, I had expected the APIs for set and finset to be completely parallel (where it makes sense). But this does not seem to be the case.
For example, there is docs#set.insert_diff_self_of_not_mem , but there is nothing corresponding to it for finsets, as far as I was able to find out. (There is docs#finset.insert_sdiff_of_mem , but this is a different statement and needs an application of docs#finset.sdiff_singleton_not_mem_eq_self to conclude).

[Yaël Dillies]

This is indeed very annoying. I've made countless PRs to parallelise them as much as possible, but the APIs are so big that it's still far from done.