fmod NAT-UTILS is

*** Operations related to natural numbers.

protecting NAT .
protecting QID .
protecting STRING .
protecting CONVERSION .

var n m : Nat .

op max : Nat Nat -> Nat .
eq max(0,0) = 0 .
eq max(0,n) = n .
eq max(n,0) = n .
eq max((s m),(s n)) = (s max(m,n)) .

op minus : Nat Nat -> Nat .
eq minus(n,0) = n .
eq minus(0,n) = 0 .
eq minus((s n),(s m)) = minus(n,m) .

*** Conversions between natural numbers and identifiers.

var qid : Qid .

op natToQid : Nat -> Qid .
eq natToQid(n) = qid(string(n,10)) .

op qidToNat : Qid -> Nat .
eq qidToNat(qid) = rat(string(qid),10) .

endfm