def le

bendtorch@1.3.0.0 · spec.bend:68

import Base

68# a <= b, by recursion (simpler to reason about than Nat.is_le, which goes through Nat.cmp)
69def le(a: Nat, b: Nat) -> Bool:
70  match a b:
71    case 0n _:
72      True{}
73    case 1n+p 0n:
74      False{}
75    case 1n+p 1n+q:
76      le(p, q)