/Prelude-v22.0.0/Natural/subtract.dhall

Copy path to clipboard

subtract m n computes n - m, truncating to 0 if m > n

Examples

subtract 1 2 ≡ 1
subtract 1 1 ≡ 0
subtract 2 1 ≡ 0

Source

--| `subtract m n` computes `n - m`, truncating to `0` if `m > n`
let subtract
: Natural → Natural → Natural
= Natural/subtract

let example0 = assert : subtract 1 2 ≡ 1

let example1 = assert : subtract 1 1 ≡ 0

let example2 = assert : subtract 2 1 ≡ 0

let property0 = λ(n : Natural) → assert : subtract 0 nn

let property1 = λ(n : Natural) → assert : subtract n 0 ≡ 0

let property2 = λ(n : Natural) → assert : subtract n n ≡ 0

in subtract