Julian Külshammer (Jan 25 2021 at 20:42):
r+bq: This is currently called
mod_add_div. (And before this PR existed for nat, pnat, int.)
bq+r: This is currently called
div_add_mod. (And before this PR existed for euclidean_domain and ordinal.)
qb+r: This currently doesn't exist, but looks to me like the most common version one would find in a text book.
r+qb: This currently doesn't exist.
In the issue, Scott just called the non-existing
mod_add_div'. In the PR review, @Eric Wieser suggested renaming all of them taking the naming convention literally and adding a
mul, so e.g. the first one would become
mod_add_mul_div. What is your opinion? Should the missing two be added? Any opinion or suggestion on the name?
Last updated: May 15 2021 at 22:14 UTC