Arith.cmp_bits: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
Lines 73-115 of bendtorch-core@0.1.0.0/src/storage/arith.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&start_line=73&end_line=115

import Base

def cmp_bits(+x: Nat, +y: Nat, +a: Bool, +b: Bool) ->
  {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(bit(a, x), bit(b, y)) : Cmp}:
  match x y:
    case 0n 0n:
      match a b:
        case False{} False{}:
          {==}
        case False{} True{}:
          {==}
        case True{} False{}:
          {==}
        case True{} True{}:
          {==}
    case 0n 1n+q:
      match a b:
        case False{} False{}:
          {==}
        case False{} True{}:
          {==}
        case True{} False{}:
          {==}
        case True{} True{}:
          {==}
    case 1n+p 0n:
      match a b:
        case False{} False{}:
          {==}
        case False{} True{}:
          {==}
        case True{} False{}:
          {==}
        case True{} True{}:
          {==}
    case 1n+p 1n+q:
      match a b:
        case False{} False{}:
          cmp_bits(p, q, False{}, False{})
        case False{} True{}:
          cmp_bits(p, q, False{}, True{})
        case True{} False{}:
          cmp_bits(p, q, True{}, False{})
        case True{} True{}:
          cmp_bits(p, q, True{}, True{})

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=bit