## Stream: Is there code for X?

### Topic: fast div and mod

#### Chris Hughes (Aug 12 2020 at 14:56):

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 (Aug 12 2020 at 15:17):

There is divmod  for pos_num already.

#### Mario Carneiro (Aug 12 2020 at 15:19):

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 (Aug 12 2020 at 15:30):

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

#### Mario Carneiro (Aug 12 2020 at 15:51):

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

Last updated: May 07 2021 at 21:10 UTC