independent and auxiliary

Stream: mathlib4

[Joseph O]

So I have this function sum, which is standalone, but I also have another function, sumBy, which with my current design idea uses sum as an auxiliary function. Is that ok in mathlib4?

[Joseph O]

Or should i do

def sumBy ... :=
    let sum := ...
    ...use local sum...

[Mario Carneiro]

Of course

[Mario Carneiro]

The point of these functions is to be used, and mathlib is one of its own biggest users

[Joseph O]

Right, but the thing is, if someone took out sum, then sumBy wouldn't work.

[Henrik Böving]

That's...an argument you can make against writing any function in the first place? That doesn't exactly make sense when you think about it in the bigger picture

[Joseph O]

I guess so

[Mario Carneiro]

It's also not really true. If someone wanted to remove sum they would inline it into sumBy first so as to not break anything

[Joseph O]

That is reassuring. Thank you.

[Joseph O]

Not really related to this channel topic, but when the real mathlib4 port starts, will this repository get deleted, or stay as a public archive?