fast div and mod

Stream: Is there code for X?

[Chris Hughes]

Is it faster to compute div and mod for integers at the same time? i.e Is there a function div_mod such that let (q, r) := div_mod a b is slightly faster than let q := a / b, let r := a % b, with a and b in int?

[Alex J. Best]

There is divmod  for pos_num already.

[Mario Carneiro]

You are basically reliant on the primitives to provide this; otherwise you can just define def divmod (a b : nat) := (a / b, a % b)

[Alex J. Best]

Wouldn't def divmod (a b : nat) := let div := a / b in (div, a - b * div)  be faster than using both % and /?

[Mario Carneiro]

Maybe. I would guess that the lean overhead of calling multiple functions is already more than the GMP bignum implementation overhead