Zulip Chat Archive

Stream: general

Topic: Name suggestions for mod_add_div' and div_add_mod'


view this post on Zulip Julian Külshammer (Jan 25 2021 at 20:42):

In #5884 I have started trying to resolve issue #1534. The basic question is to what the names of division with remainder should be (and how many of them should be there). There are four variations:

  • 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 div_add_mod and 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