pub open spec fn clip(x: int) -> nat
{ if x < 0 { 0 } else { x as nat } }
This function converts the given integer x to a natural number by returning 0 when x is negative and x otherwise.
x