nat.dist

Stream: general

[Yaël Dillies]

i just came across nat.dist and I'm a bit puzzled. It's only ever used in data.ordmap.ordset. Is it generalised by other stuff in the library? Does it matter?

[Anne Baanen]

To save others a click, dist is the symmetric distance, defined as (n - m) + (m - n) or equivalently int.nat_abs (n - m : ℤ).

[Mario Carneiro]

it is the nat version of the dist function on metric spaces (which is real-valued)

[Anne Baanen]

I don't see an issue with keeping it. There are quite a few places where we use abs (n - m) where n m are already in some ring (see e.g. usages of docs#abs_sub), but it's not immediate to go from that to nat.dist.

[Yaël Dillies]

Okay sure :smile: . I just thought that because it's now a really old file in an isolated part of the library.