{- `subtract m n` computes `n - m`. -} let Natural/lessThanEqual = ../Natural/lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99 ? ../Natural/lessThanEqual let Integer/abs = ./abs sha256:35212fcbe1e60cb95b033a4a9c6e45befca4a298aa9919915999d09e69ddced1 ? ./abs let subtract : Integer → Integer → Integer = λ(m : Integer) → λ(n : Integer) → let mAbs = Integer/abs m let nAbs = Integer/abs n let mNonPos = Natural/isZero (Integer/clamp m) let nNonPos = Natural/isZero (Integer/clamp n) let diff = if mNonPos == nNonPos then if Natural/lessThanEqual mAbs nAbs then Integer/negate (Natural/toInteger (Natural/subtract mAbs nAbs)) else Natural/toInteger (Natural/subtract nAbs mAbs) else Natural/toInteger (mAbs + nAbs) in if mNonPos then diff else Integer/negate diff let example0 = assert : subtract +3 +5 ≡ +2 let example1 = assert : subtract +4 +4 ≡ +0 let example2 = assert : subtract +5 +3 ≡ -2 let example3 = assert : subtract -3 -5 ≡ -2 let example4 = assert : subtract -4 -4 ≡ +0 let example5 = assert : subtract -5 -3 ≡ +2 let example6 = assert : subtract -3 +5 ≡ +8 let example7 = assert : subtract +3 -5 ≡ -8 let example8 = assert : subtract +0 -3 ≡ -3 in subtract