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):
Last updated: Dec 20 2023 at 11:08 UTC