def le_leb

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

import Base

595# leb is Base's Nat.is_le, case for case. leb walks its arguments one step at a time in the compiled program; Base's
596# comparison is one native comparison there (0.1.13.0).
597def le_leb(a: Nat, b: Nat) -> {Nat.is_le(a, b) == leb(a, b) : Bool}:
598  match a b:
599    case 0n 0n:
600      {==}
601    case 0n 1n+q:
602      {==}
603    case 1n+p 0n:
604      {==}
605    case 1n+p 1n+q:
606      le_leb(p, q)