Zulip Chat Archive

Stream: general

Topic: Lemma removal contest


view this post on Zulip Eric Wieser (Nov 02 2020 at 16:53):

Which of these identical lemmas should get the axe? docs#finsupp.leval' or docs#finsupp.lapply?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 02 2020 at 16:55):

Ah, but docs#eval_add_hom also exists

view this post on Zulip Eric Wieser (Nov 02 2020 at 16:56):

So lapply and apply_add_hom or leval and eval_add_hom?

view this post on Zulip Anne Baanen (Nov 02 2020 at 17:09):

finsupp.leval is doubly redundant, so keeping only lapply makes sense.

view this post on Zulip Eric Wieser (Nov 02 2020 at 17:17):

Should eval_add_hom be renamed to apply_add_hom then?

view this post on Zulip Eric Wieser (Nov 02 2020 at 17:17):

#4876


Last updated: May 13 2021 at 18:26 UTC