def leb

bend-ml-tensor-array@0.1.19.0 · main.bend:547

import Base

547# a <= b, by direct recursion
548def leb(a: Nat, b: Nat) -> Bool:
549  match a b:
550    case 0n _:
551      True{}
552    case 1n+p 0n:
553      False{}
554    case 1n+p 1n+q:
555      leb(p, q)