def LE

bend-lawful-stdlib@0.1.0.0 · src/nat.bend:27

import Base

27# a <= b, as a type: Unit when it holds, Empty when it does not.
28def LE(a: Nat, b: Nat) -> Data:
29  match a b:
30    case 0n y:
31      Unit
32    case 1n+x 0n:
33      Empty
34    case 1n+x 1n+y:
35      LE(x, y)