pub open spec fn abs(x: int) -> nat
{ if x < 0 { -x as nat } else { x as nat } }
This function computes the absolute value of a given integer.