Zulip Chat Archive

Stream: general

Topic: quotient "on_beta" vs "on_mk"


Eric Wieser (Dec 14 2020 at 20:42):

In data.quot there are two parallel naming conventions going on; both lift_on_beta and map_mk are lemmas of the form f ... (mk ...) = .... I assume this beta name is because this is a "beta" reduction, but this doesn't seem like a helpful convention considering how everything else is named.

Would i make sense to rename the _beta endings to _mk?

Eric Wieser (Dec 14 2020 at 20:43):

I ask because I wanted to add some more lemmas of this form and had no idea which convention to follow

Gabriel Ebner (Dec 14 2020 at 20:49):

(deleted)

Eric Wieser (Dec 14 2020 at 20:57):

Note the f in question is lift_on

Eric Wieser (Dec 16 2020 at 10:36):

If no one has any opposing thoughts on this rename, I'll aim to put up a PR tomorrow

Eric Wieser (Jan 27 2021 at 10:14):

#5921


Last updated: Dec 20 2023 at 11:08 UTC