E-rounding convention

Stream: general

[Martin Dvořák]

According to The Lean Language Reference, Int.ediv uses something called "E-rounding convention". Where was the phrase "E-rounding convention" first used?

[Martin Dvořák]

I guess one of the sources I can cite is:
https://dl.acm.org/doi/pdf/10.1145/128861.128862

R. T. Boute, "The Euclidean definition of the functions div and mod," ACM Transactions on Programming Languages and Systems, vol. 14, no. 2, 1992.