Zulip Chat Archive
Stream: general
Topic: Lemma removal contest
Eric Wieser (Nov 02 2020 at 16:53):
Which of these identical lemmas should get the axe? docs#finsupp.leval' or docs#finsupp.lapply?
Eric Wieser (Nov 02 2020 at 16:54):
I think I'd lean towards the former simply because it seems out of place in its file
Eric Wieser (Nov 02 2020 at 16:55):
Ah, but docs#eval_add_hom also exists
Eric Wieser (Nov 02 2020 at 16:56):
So lapply and apply_add_hom or leval and eval_add_hom?
Anne Baanen (Nov 02 2020 at 17:09):
finsupp.leval is doubly redundant, so keeping only lapply makes sense.
Eric Wieser (Nov 02 2020 at 17:17):
Should eval_add_hom be renamed to apply_add_hom then?
Eric Wieser (Nov 02 2020 at 17:17):
Last updated: Dec 20 2023 at 11:08 UTC